The continuity equation

Let E be a finite-dimensional real normed space, μ : ℝ → Measure E a family of Borel measures and v : ℝ → E → E a Borel velocity field. The continuity equation on the time interval (a, b) is ∂ₜ μₜ + div (vₜ μₜ) = 0, understood in the sense of distributions: for every smooth compactly supported test function φ : ℝ × E → ℝ whose support lies in (a, b) × E, ∫_a^b ∫_E (∂ₜ φ (t, x) + ⟨∇ₓ φ (t, x), vₜ x⟩) dμₜ(x) dt = 0. In a normed space the integrand is the space-time derivative of φ applied to the space-time velocity (1, vₜ x), that is fderiv ℝ φ (t, x) (1, v t x); this fixes the sign convention of the equation together with its test-function identity. Finite dimensionality is essential: in an infinite-dimensional space every compactly supported continuous function vanishes, so the identity would be vacuous. The definition TauCeti.IsContinuityEquation also records the measurability of the time slices t ↦ μₜ and of v, and the integrability of the total mass t ↦ μₜ E and of ∫ ‖vₜ‖ dμₜ over (a, b), which make every integral in the identity absolutely convergent.

The continuity equation is the Eulerian description of mass moving with velocity v. Its basic source of solutions is the Lagrangian one: if P is a finite measure on a parameter space Ω and γ : Ω → ℝ → E is a measurable family of absolutely continuous curves with deriv γ_ω t = vₜ (γ_ω t) for almost every (ω, t), and with finite expected length ∫ ∫_a^b ‖vₜ (γ_ω t)‖ dt dP(ω) < ∞, then the laws μₜ = (γ · t)₊ P of the positions at time t solve the continuity equation with velocity v (TauCeti.isContinuityEquation_map). For Ω a space of curves and γ the evaluation map this is the statement for a law on paths. A translating law, a stationary law and a Dirac mass moving along an absolutely continuous curve are special cases.

The curves need not follow a common velocity field. If γ_ω has derivative V ω t at almost every time, with V jointly measurable and of finite expected length, then the laws μₜ solve the continuity equation with the barycentric velocity v: its value at the position γ_ω t is the conditional expectation of V ω t given the time t and the position γ_ω t, for the measure dt ⊗ P (TauCeti.exists_isContinuityEquation_map). By Jensen's inequality, ∫_a^b ∫ ‖vₜ‖ ^ p dμₜ dt ≤ ∫ ∫_a^b ‖V ω t‖ ^ p dt dP(ω) for every p ≥ 1: the action of the velocity field is at most the expected action of the curves.

Main definitions

• TauCeti.IsContinuityEquation μ v a b: the family μ solves the continuity equation with velocity v in the sense of distributions on the time interval (a, b).

Main results

• TauCeti.IsContinuityEquation.mono: a solution on (a, b) is a solution on every subinterval.
• TauCeti.IsContinuityEquation.congr: the velocity field matters only μₜ-almost everywhere, for almost every time t.
• TauCeti.IsContinuityEquation.lintegral_lintegral_enorm_fderiv_lt_top, TauCeti.IsContinuityEquation.ae_integrable_fderiv and TauCeti.IsContinuityEquation.integrableOn_integral_fderiv: for every C¹ compactly supported test function, the integrand of the continuity equation is absolutely integrable against μₜ dt, integrable against μₜ for almost every t, and its spatial integral is integrable in time.
• TauCeti.IsContinuityEquation.integrableOn_integral_of_norm_le: the spatial integral of a bounded jointly strongly measurable function with values in a normed real vector space is integrable over (a, b).
• TauCeti.IsContinuityEquation.integrableOn_integral_fderiv_of_norm_fderiv_le: for a real-valued function with bounded derivative, the spatial integral of the integrand of the continuity equation is integrable over (a, b).
• TauCeti.isContinuityEquation_map: the laws at time t of a measurable family of absolutely continuous curves following v, with finite expected length, solve the continuity equation with velocity v.
• TauCeti.exists_isContinuityEquation_map: the laws at time t of a measurable family of absolutely continuous curves with finite expected length solve the continuity equation with their barycentric velocity, whose p-action is at most the expected p-action of the curves.
• TauCeti.isContinuityEquation_map_add_smul: a law translating with constant velocity w solves the continuity equation with velocity field w.
• TauCeti.isContinuityEquation_const: a stationary law solves it with velocity field 0.
• TauCeti.isContinuityEquation_dirac: a Dirac mass moving along an absolutely continuous curve γ solves it with any velocity field equal to deriv γ along γ.

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, and §8.3 for the barycentric velocity of a law on curves.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §4.1.

structure TauCeti.IsContinuityEquation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] (μ : ℝ → MeasureTheory.Measure E) (v : ℝ → E → E) (a b : ℝ) : Prop

The family of measures μ : ℝ → Measure E solves the continuity equation ∂ₜ μₜ + div (vₜ μₜ) = 0 with velocity field v on the time interval (a, b), in the sense of distributions: for every smooth compactly supported φ : ℝ × E → ℝ with support in (a, b) × E, ∫_a^b ∫ (∂ₜ φ (t, x) + ⟨∇ₓ φ (t, x), vₜ x⟩) dμₜ(x) dt = 0, the integrand being written as the space-time derivative fderiv ℝ φ (t, x) applied to (1, v t x). The time slices t ↦ μₜ and the velocity field are measurable, and the total mass and ∫ ‖vₜ‖ dμₜ are integrable over (a, b). The space E is finite-dimensional with its Borel σ-algebra, so that the test functions separate measures and every integrand in the identity is measurable.

• measurable : Measurable μ

  The time slices t ↦ μₜ form a measurable family of measures.

• measurable_velocity : Measurable (Function.uncurry v)

  The velocity field is jointly measurable in time and space.

• lintegral_measure_univ_lt_top : ∫⁻ (t : ℝ) in Set.Ioo a b, (μ t) Set.univ < ⊤

  The total mass of μₜ is integrable over the time interval.

• lintegral_lintegral_enorm_lt_top : ∫⁻ (t : ℝ) in Set.Ioo a b, ∫⁻ (x : E), ‖v t x‖ₑ ∂μ t < ⊤

  The velocity field is integrable against μₜ dt.

• integral_integral_fderiv_eq_zero ⦃φ : ℝ × E → ℝ⦄ (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφs : tsupport φ ⊆ Set.Ioo a b ×ˢ Set.univ) : ∫ (t : ℝ) in Set.Ioo a b, ∫ (x : E), (fderiv ℝ φ (t, x)) (1, v t x) ∂μ t = 0

  The distributional identity ∫_a^b ∫ (∂ₜ φ + ⟨∇ₓ φ, vₜ⟩) dμₜ dt = 0.

theorem TauCeti.IsContinuityEquation.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : ℝ → MeasureTheory.Measure E} {v : ℝ → E → E} {a b c d : ℝ} (h : IsContinuityEquation μ v a b) (hac : a ≤ c) (hdb : d ≤ b) : IsContinuityEquation μ v c d

A solution of the continuity equation on (a, b) solves it on every subinterval (c, d).

theorem TauCeti.IsContinuityEquation.congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : ℝ → MeasureTheory.Measure E} {v w : ℝ → E → E} {a b : ℝ} (h : IsContinuityEquation μ v a b) (hw : Measurable (Function.uncurry w)) (hvw : ∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → v t =ᵐ[μ t] w t) : IsContinuityEquation μ w a b

The velocity field of a solution of the continuity equation matters only μₜ-almost everywhere, for almost every time t: replacing it by a measurable field which agrees with it there gives another solution.

theorem TauCeti.IsContinuityEquation.lintegral_lintegral_enorm_fderiv_lt_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : ℝ → MeasureTheory.Measure E} {v : ℝ → E → E} {a b : ℝ} (h : IsContinuityEquation μ v a b) {φ : ℝ × E → ℝ} (hφ : ContDiff ℝ 1 φ) (hφc : HasCompactSupport φ) : ∫⁻ (t : ℝ) in Set.Ioo a b, ∫⁻ (x : E), ‖(fderiv ℝ φ (t, x)) (1, v t x)‖ₑ ∂μ t < ⊤

The integrand of the continuity equation is absolutely integrable against μₜ dt on (a, b), for every C¹ compactly supported test function φ.

theorem TauCeti.IsContinuityEquation.ae_integrable_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : ℝ → MeasureTheory.Measure E} {v : ℝ → E → E} {a b : ℝ} (h : IsContinuityEquation μ v a b) {φ : ℝ × E → ℝ} (hφ : ContDiff ℝ 1 φ) (hφc : HasCompactSupport φ) : ∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → MeasureTheory.Integrable (fun (x : E) => (fderiv ℝ φ (t, x)) (1, v t x)) (μ t)

For almost every time t ∈ (a, b), the integrand of the continuity equation is integrable against μₜ, for every C¹ compactly supported test function φ.

theorem TauCeti.IsContinuityEquation.integrableOn_integral_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : ℝ → MeasureTheory.Measure E} {v : ℝ → E → E} {a b : ℝ} (h : IsContinuityEquation μ v a b) {φ : ℝ × E → ℝ} (hφ : ContDiff ℝ 1 φ) (hφc : HasCompactSupport φ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ∫ (x : E), (fderiv ℝ φ (t, x)) (1, v t x) ∂μ t) (Set.Ioo a b) MeasureTheory.volume

The spatial integral of the integrand of the continuity equation is integrable over (a, b), for every C¹ compactly supported test function φ.

theorem TauCeti.IsContinuityEquation.ae_isFiniteMeasure_and_integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : ℝ → MeasureTheory.Measure E} {v : ℝ → E → E} {a b : ℝ} (h : IsContinuityEquation μ v a b) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), MeasureTheory.IsFiniteMeasure (μ t) ∧ MeasureTheory.Integrable (v t) (μ t)

For almost every time t ∈ (a, b), the slice μₜ is finite and vₜ is μₜ-integrable.

theorem TauCeti.IsContinuityEquation.integrableOn_measureReal_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : ℝ → MeasureTheory.Measure E} {v : ℝ → E → E} {a b : ℝ} (h : IsContinuityEquation μ v a b) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (μ t).real Set.univ) (Set.Ioo a b) MeasureTheory.volume

The total mass of μₜ is integrable over (a, b).

theorem TauCeti.IsContinuityEquation.integrableOn_integral_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : ℝ → MeasureTheory.Measure E} {v : ℝ → E → E} {a b : ℝ} (h : IsContinuityEquation μ v a b) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ∫ (x : E), ‖v t x‖ ∂μ t) (Set.Ioo a b) MeasureTheory.volume

The μₜ-integral of ‖vₜ‖ is integrable over (a, b).

theorem TauCeti.IsContinuityEquation.integrableOn_integral_of_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [BorelSpace E] {μ : ℝ → MeasureTheory.Measure E} {v : ℝ → E → E} {a b : ℝ} (h : IsContinuityEquation μ v a b) {f : ℝ × E → F} (hf : MeasureTheory.StronglyMeasurable f) {M : ℝ} (hM : ∀ (q : ℝ × E), ‖f q‖ ≤ M) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ∫ (x : E), f (t, x) ∂μ t) (Set.Ioo a b) MeasureTheory.volume

For a bounded jointly strongly measurable function f of time and space with values in a normed real vector space, the function t ↦ ∫ f (t, x) dμₜ(x) is integrable over (a, b).

theorem TauCeti.IsContinuityEquation.integrableOn_integral_fderiv_of_norm_fderiv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : ℝ → MeasureTheory.Measure E} {v : ℝ → E → E} {a b : ℝ} (h : IsContinuityEquation μ v a b) {u : ℝ × E → ℝ} {M : ℝ} (hM : ∀ (q : ℝ × E), ‖fderiv ℝ u q‖ ≤ M) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ∫ (x : E), (fderiv ℝ u (t, x)) (1, v t x) ∂μ t) (Set.Ioo a b) MeasureTheory.volume

For a function u of time and space with bounded derivative, the spatial integral t ↦ ∫ fderiv ℝ u (t, x) (1, vₜ x) dμₜ(x) of the integrand of the continuity equation is integrable over (a, b).

theorem TauCeti.isContinuityEquation_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {v : ℝ → E → E} {a b : ℝ} {Ω : Type u_3} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] {γ : Ω → ℝ → E} (hγ : Measurable (Function.uncurry γ)) (hv : Measurable (Function.uncurry v)) (hac : ∀ᵐ (ω : Ω) ∂P, AbsolutelyContinuousOnInterval (γ ω) a b) (hderiv : ∀ᵐ (ω : Ω) ∂P, ∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → HasDerivAt (γ ω) (v t (γ ω t)) t) (hint : ∫⁻ (ω : Ω), ∫⁻ (t : ℝ) in Set.Ioo a b, ‖v t (γ ω t)‖ₑ ∂P < ⊤) : IsContinuityEquation (fun (t : ℝ) => MeasureTheory.Measure.map (fun (x : Ω) => γ x t) P) v a b

Lagrangian solutions of the continuity equation. Let P be a finite measure on a parameter space Ω and γ : Ω → ℝ → E a jointly measurable family of curves. If P-almost every curve is absolutely continuous on [a, b] and follows the velocity field v, in the sense that deriv γ_ω t = vₜ (γ_ω t) for almost every t ∈ (a, b), and the expected length ∫ ∫_a^b ‖vₜ (γ_ω t)‖ dt dP(ω) is finite, then the laws (γ · t)₊ P of the positions at time t solve the continuity equation with velocity v on (a, b).

theorem TauCeti.exists_isContinuityEquation_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {a b : ℝ} {Ω : Type u_3} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] {γ V : Ω → ℝ → E} (hγ : Measurable (Function.uncurry γ)) (hV : Measurable (Function.uncurry V)) (hac : ∀ᵐ (ω : Ω) ∂P, AbsolutelyContinuousOnInterval (γ ω) a b) (hderiv : ∀ᵐ (ω : Ω) ∂P, ∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → HasDerivAt (γ ω) (V ω t) t) (hint : ∫⁻ (ω : Ω), ∫⁻ (t : ℝ) in Set.Ioo a b, ‖V ω t‖ₑ ∂P < ⊤) : ∃ (v : ℝ → E → E), IsContinuityEquation (fun (t : ℝ) => MeasureTheory.Measure.map (fun (x : Ω) => γ x t) P) v a b ∧ (fun (q : ℝ × Ω) => v q.1 (γ q.2 q.1)) = ((MeasureTheory.volume.restrict (Set.Ioo a b)).prod P)[fun (q : ℝ × Ω) => V q.2 q.1 | MeasurableSpace.comap (fun (q : ℝ × Ω) => (q.1, γ q.2 q.1)) inferInstance] ∧ ∀ (p : ℝ), 1 ≤ p → ∫⁻ (t : ℝ) in Set.Ioo a b, ∫⁻ (x : E), ‖v t x‖ₑ ^ p ∂MeasureTheory.Measure.map (fun (x : Ω) => γ x t) P ≤ ∫⁻ (ω : Ω), ∫⁻ (t : ℝ) in Set.Ioo a b, ‖V ω t‖ₑ ^ p ∂P

The barycentric velocity of a law on curves. Let P be a finite measure on a parameter space Ω and γ : Ω → ℝ → E a jointly measurable family of curves, P-almost every one of which is absolutely continuous on [a, b] with derivative V ω t at almost every t ∈ (a, b), where V is jointly measurable with finite expected length ∫ ∫_a^b ‖V ω t‖ dt dP(ω). Then the laws μₜ = (γ · t)₊ P of the positions at time t solve the continuity equation on (a, b) with a velocity field v whose value at the position γ ω t is the conditional expectation of the velocity V ω t given the time and the position, for the measure dt ⊗ P on (a, b) × Ω. By Jensen's inequality its action is at most the expected action of the curves: ∫_a^b ∫ ‖vₜ‖ ^ p dμₜ dt ≤ ∫ ∫_a^b ‖V ω t‖ ^ p dt dP(ω) for every p ≥ 1.

Unlike TauCeti.isContinuityEquation_map, the curves need not follow a common velocity field: curves crossing at the same position at the same time may have different velocities there, which the conditional expectation averages.

theorem TauCeti.isContinuityEquation_map_add_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasure μ] (w : E) (a b : ℝ) : IsContinuityEquation (fun (t : ℝ) => MeasureTheory.Measure.map (fun (x : E) => x + t • w) μ) (fun (x : ℝ) (x_1 : E) => w) a b

A translating law solves the continuity equation. Translating a finite measure μ with constant velocity w, so that its law at time t is the pushforward of μ by x ↦ x + t • w, solves the continuity equation with the constant velocity field w.

theorem TauCeti.isContinuityEquation_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasure μ] (a b : ℝ) : IsContinuityEquation (fun (x : ℝ) => μ) (fun (x : ℝ) (x_1 : E) => 0) a b

A stationary law solves the continuity equation. A finite measure which does not move solves the continuity equation with velocity field 0.

theorem TauCeti.isContinuityEquation_dirac {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {v : ℝ → E → E} {a b : ℝ} {γ : ℝ → E} (hγm : Measurable γ) (hγ : AbsolutelyContinuousOnInterval γ a b) (hv : Measurable (Function.uncurry v)) (hderiv : ∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → HasDerivAt γ (v t (γ t)) t) : IsContinuityEquation (fun (t : ℝ) => MeasureTheory.Measure.dirac (γ t)) v a b

A moving Dirac mass solves the continuity equation. If γ is a measurable curve which is absolutely continuous on [a, b] and v is a measurable velocity field with deriv γ t = vₜ (γ t) for almost every t ∈ (a, b), then the Dirac masses δ_{γ t} solve the continuity equation with velocity v on (a, b). The finite length ∫_a^b ‖vₜ (γ t)‖ dt < ∞ follows from absolute continuity in finite dimension.