The continuity equation with boundary-time terms

The definition TauCeti.IsContinuityEquation tests the continuity equation ∂ₜ μₜ + div (vₜ μₜ) = 0 on (a, b) only against test functions supported in (a, b) × E, and says nothing about the measures at the times a and b. This file removes the support condition in time, at the cost of boundary terms. For a bounded C¹ function u : ℝ × E → ℝ with bounded derivative, the function t ↦ ∫ u (t, x) dμₜ(x) has weak derivative

t ↦ ∫ (∂ₜ u (t, x) + ⟨∇ₓ u (t, x), vₜ x⟩) dμₜ(x)

on (a, b), integrable there (TauCeti.IsContinuityEquation.hasWeakLineDerivOn_integral). So t ↦ ∫ u (t, ·) dμₜ agrees almost everywhere with a constant plus a primitive of its weak derivative. If t ↦ μₜ is a curve of finite measures that is narrowly continuous on [a, b], then t ↦ ∫ u (t, ·) dμₜ is continuous on [a, b] and agrees with that function everywhere there: for all s, t ∈ [a, b],

∫ u (t, x) dμₜ(x) - ∫ u (s, x) dμₛ(x) = ∫_s^t ∫ (∂ₜ u (r, x) + ⟨∇ₓ u (r, x), vᵣ x⟩) dμᵣ(x) dr

(TauCeti.IsContinuityEquation.intervalIntegral_integral_fderiv_eq_sub). The integrand is written, as in TauCeti.IsContinuityEquation, as the space-time derivative fderiv ℝ u (r, x) applied to (1, v r x).

This is the form in which a solution of the continuity equation joins its endpoint laws μ a and μ b. In particular, if u is a subsolution of a Hamilton–Jacobi equation, in the sense that ∂ₜ u (t, x) + ⟨∇ₓ u (t, x), w⟩ ≤ L w for every velocity w, the identity bounds ∫ u (b, ·) d(μ b) - ∫ u (a, ·) d(μ a) by the action ∫_a^b ∫ L (vₜ x) dμₜ(x) dt; this is how dual formulations of transport costs are compared with the action of a velocity field.

Main results

• TauCeti.IsContinuityEquation.hasWeakLineDerivOn_integral: for a bounded C¹ function u with bounded derivative, t ↦ ∫ u (t, ·) dμₜ has weak derivative t ↦ ∫ (∂ₜ u + ⟨∇ₓ u, vₜ⟩) dμₜ on (a, b).
• TauCeti.IsContinuityEquation.intervalIntegral_integral_fderiv_eq_sub: along a narrowly continuous curve of finite measures, the continuity equation integrated from s to t against such a u equals the difference of the boundary terms ∫ u (t, ·) dμₜ - ∫ u (s, ·) dμₛ.
• TauCeti.IsContinuityEquation.measure_univ_eq: such a curve conserves its total mass on [a, b].

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, Lemma 8.1.2.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §4.1.

theorem TauCeti.IsContinuityEquation.hasWeakLineDerivOn_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {v : ℝ → E → E} {a b : ℝ} {u : ℝ × E → ℝ} {M M' : ℝ} {μ : ℝ → MeasureTheory.Measure E} (h : IsContinuityEquation μ v a b) (hu : ContDiff ℝ 1 u) (huM : ∀ (q : ℝ × E), ‖u q‖ ≤ M) (hDu : ∀ (q : ℝ × E), ‖fderiv ℝ u q‖ ≤ M') : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } (fun (t : ℝ) => ∫ (x : E), u (t, x) ∂μ t) (fun (t : ℝ) => ∫ (x : E), (fderiv ℝ u (t, x)) (1, v t x) ∂μ t) 1

The weak time derivative along a solution. For a bounded C¹ function u of time and space with bounded derivative, the function t ↦ ∫ u (t, x) dμₜ(x) has weak derivative t ↦ ∫ (∂ₜ u (t, x) + ⟨∇ₓ u (t, x), vₜ x⟩) dμₜ(x) on (a, b), the integrand being written as the space-time derivative fderiv ℝ u (t, x) applied to (1, v t x).

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

The continuity equation with boundary-time terms. Let t ↦ νₜ be a curve of finite measures, narrowly continuous on [a, b], solving the continuity equation with velocity v on (a, b). For every bounded C¹ function u of time and space with bounded derivative and all s, t ∈ [a, b], ∫_s^t ∫ (∂ₜ u (r, x) + ⟨∇ₓ u (r, x), vᵣ x⟩) dνᵣ(x) dr = ∫ u (t, x) dνₜ(x) - ∫ u (s, x) dνₛ(x), the integrand being written as the space-time derivative fderiv ℝ u (r, x) applied to (1, v r x).

theorem TauCeti.IsContinuityEquation.measure_univ_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {v : ℝ → E → E} {a b : ℝ} {ν : ℝ → MeasureTheory.FiniteMeasure E} (h : IsContinuityEquation (fun (t : ℝ) => ↑(ν t)) v a b) (hν : ContinuousOn ν (Set.Icc a b)) {s t : ℝ} (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) : ↑(ν t) Set.univ = ↑(ν s) Set.univ

Conservation of mass. A curve t ↦ νₜ of finite measures, narrowly continuous on [a, b] and solving the continuity equation on (a, b), has the same total mass at all times in [a, b]: νₜ E = νₛ E. This is the continuity equation with boundary-time terms tested against the constant function 1.