Test functions for the continuity equation

The definition TauCeti.IsContinuityEquation tests the continuity equation ∂ₜ μₜ + div (vₜ μₜ) = 0 on (a, b) only against smooth compactly supported functions φ : ℝ × E → ℝ with support in (a, b) × E. The functions built in practice from a solution are seldom of this kind: composing with the flow of a C¹ velocity field gives only C¹ functions, and convolving with an everywhere positive kernel, or testing against a bounded function of space alone, gives functions without compact support in space. This file shows that the distributional identity

∫_a^b ∫ (∂ₜ φ (t, x) + ⟨∇ₓ φ (t, x), vₜ x⟩) dμₜ(x) dt = 0

holds for every C¹ function φ with bounded derivative and support in (a, b) × E, with no compactness of the support in space. Such a φ is automatically bounded, since it vanishes at the time a; the integrability built into TauCeti.IsContinuityEquation of the total mass and of ‖vₜ‖ against μₜ dt is exactly what makes the identity absolutely convergent.

The proof has two approximation steps, each closed by dominated convergence. A C¹ compactly supported test function is the limit of its convolutions with shrinking normalized smooth bumps, which are smooth, compactly supported, have support in (a, b) × E once the bump is small, and have derivatives converging pointwise with a uniform bound. A C¹ test function with bounded derivative is the limit of its products with the spatial cut-offs x ↦ χ (x / R) for a fixed bump χ equal to 1 near 0, whose derivatives are of size 1 / R.

Main results

• TauCeti.IsContinuityEquation.integral_integral_fderiv_eq_zero_of_hasCompactSupport: the continuity equation holds against every C¹ compactly supported test function with support in (a, b) × E.
• TauCeti.IsContinuityEquation.integral_integral_fderiv_eq_zero_of_norm_fderiv_le: it holds against every C¹ test function with bounded derivative and support in (a, b) × E.
• TauCeti.IsContinuityEquation.integral_deriv_mul_integral_eq_neg: for a bounded C¹ function u of time and space with bounded derivative, the weak time derivative of t ↦ ∫ u (t, ·) dμₜ on (a, b) is t ↦ ∫ (∂ₜ u + ⟨∇ₓ u, vₜ⟩) dμₜ.

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, equations (8.1.3) and (8.1.4).
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §4.1.

theorem TauCeti.IsContinuityEquation.integral_integral_fderiv_eq_zero_of_hasCompactSupport {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 φ) (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 continuity equation holds against every C¹ compactly supported test function with support in (a, b) × E, not only against smooth ones. For test functions without compact support see TauCeti.IsContinuityEquation.integral_integral_fderiv_eq_zero_of_norm_fderiv_le.

theorem TauCeti.IsContinuityEquation.integral_integral_fderiv_eq_zero_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) {φ : ℝ × E → ℝ} (hφ : ContDiff ℝ 1 φ) {C : ℝ} (hC : ∀ (q : ℝ × E), ‖fderiv ℝ φ q‖ ≤ C) (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

Test functions with bounded derivative. The continuity equation holds against every C¹ test function φ with bounded derivative and support in (a, b) × E, with no compactness of the support in space. Such a φ is bounded, since it vanishes at the time a.

theorem TauCeti.IsContinuityEquation.integral_deriv_mul_integral_eq_neg {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) {η : ℝ → ℝ} (hη : ContDiff ℝ 1 η) (hηs : tsupport η ⊆ Set.Ioo a b) {u : ℝ × E → ℝ} (hu : ContDiff ℝ 1 u) {M M' : ℝ} (huM : ∀ (q : ℝ × E), ‖u q‖ ≤ M) (hDu : ∀ (q : ℝ × E), ‖fderiv ℝ u q‖ ≤ M') : ∫ (t : ℝ) in Set.Ioo a b, deriv η t * ∫ (x : E), u (t, x) ∂μ t = -∫ (t : ℝ) in Set.Ioo a b, η t * ∫ (x : E), (fderiv ℝ u (t, x)) (1, v t x) ∂μ t

The weak time derivative of t ↦ ∫ u (t, ·) dμₜ. 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): for every C¹ function η with support in (a, b), ∫_a^b η' (t) ∫ u (t, x) dμₜ(x) dt = - ∫_a^b η (t) ∫ fderiv ℝ u (t, x) (1, vₜ x) dμₜ(x) dt.