Hamilton–Jacobi subsolutions along the continuity equation

Let t ↦ νₜ be a curve of finite measures on a finite-dimensional real normed space E, narrowly continuous on [a, b], solving the continuity equation ∂ₜ νₜ + div (vₜ νₜ) = 0 on (a, b), and let L : E → ℝ be a Lagrangian. A function u : ℝ × E → ℝ is a subsolution of the Hamilton–Jacobi equation ∂ₜ u + H (∇ₓ u) = 0, with H the convex conjugate of L, when ∂ₜ u (t, x) + ⟨∇ₓ u (t, x), w⟩ ≤ L w for every velocity w. Testing the continuity equation against a subsolution bounds its boundary terms by the action of the velocity field:

∫ u (b, ·) dν_b - ∫ u (a, ·) dν_a ≤ ∫_a^b ∫ L (vₜ x) dνₜ(x) dt.

The left side is a Kantorovich dual value when u (a, ·) and u (b, ·) are dual potentials for a transport cost, and for L w = ‖w‖ ^ p the right side is the p-action of v. This is the inequality behind the lower bound W_p (ν_a, ν_b) ^ p ≤ ∫_a^b ∫ ‖vₜ‖ ^ p dνₜ dt of the Benamou–Brenier formula, whose subsolutions are Hopf–Lax functions.

For a C¹ subsolution with bounded values and derivative, the inequality is the integrated continuity equation TauCeti.IsContinuityEquation.intervalIntegral_integral_fderiv_eq_sub. Hopf–Lax functions are not differentiable, and satisfy the subsolution inequality only in the difference form u (q + s • (1, w)) ≤ u q + s * L w for s > 0. The inequality still holds for a bounded measurable u satisfying this difference form on a strip (a - r, b + r) × E, provided u is upper semicontinuous at almost every point of the initial slice {a} × E and lower semicontinuous at almost every point of the final slice {b} × E. Its space-time mollifications are bounded C¹ subsolutions with bounded derivative (HasCompactSupport.fderiv_convolution_left_apply_le). As the mollifier shrinks, they are eventually almost below u on the initial slice and almost above u on the final slice (MeasureTheory.eventually_convolution_lsmul_lt_of_upperSemicontinuousAt and MeasureTheory.eventually_lt_convolution_lsmul_of_lowerSemicontinuousAt), which is the direction the inequality needs. Hopf–Lax functions satisfy the difference form only at positive times, and this is proved for the Lagrangian ‖·‖ ^ p with 1 ≤ p and a bounded-below initial datum (TauCeti.hopfLax_norm_rpow_add_add_smul_le). They are upper semicontinuous at positive times when the initial datum and the Lagrangian are bounded below and the Lagrangian is continuous (TauCeti.upperSemicontinuousOn_hopfLax). So they must be shifted in time, to make the strip lie in positive times, before this theorem applies to them. Lower semicontinuity on the final slice needs more: in a finite-dimensional space a continuous bounded initial datum makes them continuous at positive times (TauCeti.continuousOn_hopfLax_norm_rpow), which is how the lower bound of the Benamou–Brenier formula is proved (TauCeti.IsContinuityEquation.wassersteinEDist_rpow_le).

The right side is the ℝ≥0∞-valued integral of the positive part of L (vₜ x), so neither the integrability of the action nor a sign condition on L is assumed.

Main results

• TauCeti.IsContinuityEquation.ofReal_integral_sub_integral_le_lintegral_of_fderiv_le: the action bounds the boundary terms of a bounded C¹ subsolution with bounded derivative.
• TauCeti.IsContinuityEquation.ofReal_integral_sub_integral_le_lintegral_of_add_smul_le: the same bound for a bounded measurable subsolution in difference form, upper semicontinuous almost everywhere on the initial slice and lower semicontinuous almost everywhere on the final one.

References

• L. Ambrosio, N. Gigli and G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, Birkhäuser, 2nd ed. 2008, §8.1.
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 7.

theorem TauCeti.IsContinuityEquation.ofReal_integral_sub_integral_le_lintegral_of_fderiv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {v : ℝ → E → E} {a b : ℝ} {u : ℝ × E → ℝ} {M M' : ℝ} {L : E → ℝ} {ν : ℝ → MeasureTheory.FiniteMeasure E} (h : IsContinuityEquation (fun (t : ℝ) => ↑(ν t)) v a b) (hν : ContinuousOn ν (Set.Icc a b)) (hab : a ≤ b) (hu : ContDiff ℝ 1 u) (huM : ∀ (q : ℝ × E), ‖u q‖ ≤ M) (hDu : ∀ (q : ℝ × E), ‖fderiv ℝ u q‖ ≤ M') (hsub : ∀ t ∈ Set.Ioo a b, ∀ (x w : E), (fderiv ℝ u (t, x)) (1, w) ≤ L w) : ENNReal.ofReal (∫ (x : E), u (b, x) ∂↑(ν b) - ∫ (x : E), u (a, x) ∂↑(ν a)) ≤ ∫⁻ (t : ℝ) in Set.Ioo a b, ∫⁻ (x : E), ENNReal.ofReal (L (v t x)) ∂↑(ν t)

Smooth subsolutions. Let t ↦ νₜ be a curve of finite measures, narrowly continuous on [a, b], solving the continuity equation with velocity v on (a, b). For a bounded C¹ function u of time and space with bounded derivative such that ∂ₜ u (t, x) + ⟨∇ₓ u (t, x), w⟩ ≤ L w for every t ∈ (a, b), every x and every velocity w, the boundary terms are bounded by the action of v: ∫ u (b, ·) dν_b - ∫ u (a, ·) dν_a ≤ ∫_a^b ∫ L (vₜ x) dνₜ(x) dt, in the positive-part form.

theorem TauCeti.IsContinuityEquation.ofReal_integral_sub_integral_le_lintegral_of_add_smul_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {v : ℝ → E → E} {a b : ℝ} {u : ℝ × E → ℝ} {M : ℝ} {L : E → ℝ} {ν : ℝ → MeasureTheory.FiniteMeasure E} (h : IsContinuityEquation (fun (t : ℝ) => ↑(ν t)) v a b) (hν : ContinuousOn ν (Set.Icc a b)) (hab : a ≤ b) (hu : Measurable u) (huM : ∀ (q : ℝ × E), ‖u q‖ ≤ M) (hua : ∀ᵐ (x : E) ∂↑(ν a), UpperSemicontinuousAt u (a, x)) (hub : ∀ᵐ (x : E) ∂↑(ν b), LowerSemicontinuousAt u (b, x)) {r : ℝ} (hr : 0 < r) (hsub : ∀ (w : E), ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (q : ℝ × E), q.1 ∈ Set.Ioo (a - r) (b + r) → u (q + s • (1, w)) ≤ u q + s * L w) : ENNReal.ofReal (∫ (x : E), u (b, x) ∂↑(ν b) - ∫ (x : E), u (a, x) ∂↑(ν a)) ≤ ∫⁻ (t : ℝ) in Set.Ioo a b, ∫⁻ (x : E), ENNReal.ofReal (L (v t x)) ∂↑(ν t)

Subsolutions in difference form. Let t ↦ νₜ be a curve of finite measures, narrowly continuous on [a, b], solving the continuity equation with velocity v on (a, b). Let u be a bounded measurable function of time and space, upper semicontinuous at almost every point of the initial slice {a} × E and lower semicontinuous at almost every point of the final slice {b} × E, such that for some r > 0 and every velocity w, for all small s > 0, u (q + s • (1, w)) ≤ u q + s * L w at every point q of the strip (a - r, b + r) × E. Then the boundary terms are bounded by the action of v: ∫ u (b, ·) dν_b - ∫ u (a, ·) dν_a ≤ ∫_a^b ∫ L (vₜ x) dνₜ(x) dt, in the positive-part form.