The distributional fundamental theorem of calculus, and the comparison energy inequality

CIV.Comparison.EnergyInequality proves the two easy pieces of the Grönwall step of lem:aniso:comparison — the support/integrability facts about comparisonEnergy and the integral-form Grönwall inequality itself — with the integrated energy inequality eq:aniso:comparison:positive:energy as a hypothesis (hineq of comparisonEnergy_le_exp_mul_integral_sq). That integrated inequality is obtained from the mollified equation eq:aniso:comparison:mollified (mollified_equation) in three stages: (1) upgrading the time-tested identity mollified_equation delivers into the fundamental-theorem-of-calculus statement that the mollified slice is the primitive of the right side of eq:aniso:comparison:mollified; (2) a Green identity and energy computation testing that identity against (q_ε - Ψ_σ)_+, which is only Lipschitz; (3) passing to the limit in a regularization parameter. This module proves stage (1) completely, in the generality needed to feed mollified_equation's exact conclusion shape.

Main result

eq_add_intervalIntegral_of_pairing_eq: if f is continuous on an open, order connected I, h is locally integrable on I, and f obeys the tested identity ∫ f (-χ') = ∫ χ h for every χ that is ContDiff ℝ (⊤ : ℕ∞), compactly supported, with support in I — the shape mollified_equation delivers with f τ = q_ε(x, τ) and h the right side of eq:aniso:comparison:mollified at a fixed x — then f is literally the primitive of h: f τ = f τ₀ + ∫ s in τ₀..τ, h s for every τ₀, τ ∈ I.

The proof decomposes an arbitrary smooth compactly supported test function ρ against a fixed reference bump β (∫ β = 1, built from ContDiffBump) into a mean-zero part and a multiple of β. The mean-zero part is the negative derivative of a compactly supported primitive (exists_contDiff_hasCompactSupport_deriv_eq_neg_of_integral_eq_zero), so the hypothesis applies to it directly; the primitive F of h obeys the same tested identity against that same χ (integral_primitive_mul_deriv_eq_integral_mul_of_isOpen), proved through the integration by parts already in Mathlib for AbsolutelyContinuousOnInterval functions together with the interval form of the Lebesgue differentiation theorem (IntervalIntegrable.ae_hasDerivAt_integral) — not a hand Fubini argument. Comparing the two identities and testing again against β pins f - F to a constant on I via ae_eq_zero_of_integral_contDiff_smul_eq_zero, and evaluating at τ₀ shows that constant is 0.

Use

eq_add_intervalIntegral_of_pairing_eq is applied to mollified_equation in CIV.mollifySlice_eq_add_intervalIntegral, which takes continuity in time of the mollified slice and local integrability of the mollified right side as explicit hypotheses. CIV.ae_ae_sub_eq_intervalIntegral_of_pairing_eq is the almost-everywhere version without the continuity hypothesis; it gives CIV.mollifySlice_ae_ae_sub_eq_intervalIntegral from the hypotheses of the comparison lemma alone.

For stages (2)-(3), note that the natural closed form for the Kato regularization, Φ_κ(g) = (g + √(g² + κ²)) / 2 − κ/2, does not tend to 0 as g → -∞: it tends to -κ/2. Once v_ε = (q_ε - Ψ_σ)_+ is compactly supported and Φ_κ is applied to q_ε - Ψ_σ directly (which is unbounded below away from the support of v_ε), the energy ∫ Φ_κ(q_ε - Ψ_σ)² over all of Vec m is not finite for a fixed κ > 0, since the integrand tends to the nonzero constant κ²/4 at spatial infinity while Vec m has infinite measure. CIV.Comparison.EnergyInequality3 therefore applies a κ-independent spatial truncation (CIV.mollifierCutoff) before the Kato step.

theorem CIV.exists_Icc_subset_of_isCompact {s : Set ℝ} (hs : IsCompact s) (hne : s.Nonempty) : ∃ p ∈ s, ∃ q ∈ s, s ⊆ Set.Icc p q

A nonempty compact set of reals lies in the closed interval spanned by its own least and greatest elements.

theorem CIV.exists_lt_mem_of_isOpen {I : Set ℝ} (hI : IsOpen I) {p : ℝ} (hp : p ∈ I) : ∃ p' < p, p' ∈ I

A point of an open set has a strictly smaller neighbour still inside the set.

theorem CIV.exists_gt_mem_of_isOpen {I : Set ℝ} (hI : IsOpen I) {q : ℝ} (hq : q ∈ I) : ∃ q' > q, q' ∈ I

A point of an open set has a strictly larger neighbour still inside the set.

theorem CIV.tsupport_subset_of_eq_zero_of_notMem {f : ℝ → ℝ} {K : Set ℝ} (hK : IsClosed K) (hf : ∀ x ∉ K, f x = 0) : tsupport f ⊆ K

A function vanishing off a closed set has its topological support inside that set.

theorem CIV.exists_contDiff_hasCompactSupport_deriv_eq_neg_of_integral_eq_zero {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψI : tsupport ψ ⊆ I) (hmean : ∫ (τ : ℝ), ψ τ = 0) : ∃ (χ : ℝ → ℝ), ContDiff ℝ (↑⊤) χ ∧ HasCompactSupport χ ∧ tsupport χ ⊆ I ∧ deriv χ = -ψ

A smooth, mean-zero, compactly supported function with support inside an open, order connected I is the negative derivative of a smooth compactly supported function with support still inside I.

theorem CIV.integral_primitive_mul_deriv_eq_integral_mul (f0 : ℝ) {a b τ₀ : ℝ} (hab : a ≤ b) (hτ₀ : τ₀ ∈ Set.Icc a b) {h : ℝ → ℝ} (hh : IntervalIntegrable h MeasureTheory.volume a b) {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχab : tsupport χ ⊆ Set.Ioo a b) : ∫ (τ : ℝ) in a..b, (f0 + ∫ (s : ℝ) in τ₀..τ, h s) * -deriv χ τ = ∫ (τ : ℝ) in a..b, χ τ * h τ

The primitive of an interval-integrable h obeys the same test-function pairing against a smooth χ vanishing at the two ends of a..b as h itself does against χ: this is the "integration by parts against the primitive" step of the distributional fundamental theorem of calculus.

theorem CIV.intervalIntegral_eq_integral_of_forall_compl_eq_zero {a b : ℝ} (hab : a ≤ b) {g : ℝ → ℝ} (hg : ∀ x ∉ Set.Icc a b, g x = 0) : ∫ (τ : ℝ) in a..b, g τ = ∫ (τ : ℝ), g τ

A function vanishing off a set integrates the same way over that set (as an interval integral) as it does over the whole line, once the set is Icc a b.

theorem CIV.integral_primitive_mul_deriv_eq_integral_mul_of_isOpen (f0 : ℝ) {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {τ₀ : ℝ} (hτ₀ : τ₀ ∈ I) {h : ℝ → ℝ} (hh : MeasureTheory.LocallyIntegrableOn h I MeasureTheory.volume) {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) (hχI : tsupport χ ⊆ I) : ∫ (τ : ℝ), (f0 + ∫ (s : ℝ) in τ₀..τ, h s) * -deriv χ τ = ∫ (τ : ℝ), χ τ * h τ

The full-line form of integral_primitive_mul_deriv_eq_integral_mul: for h locally integrable on an open, order connected I and χ a smooth compactly supported test function with support in I, the primitive of h based at τ₀ ∈ I pairs with -χ' exactly as h pairs with χ.

theorem CIV.exists_Icc_subset_isOpen_of_mem_mem {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {x y : ℝ} (hx : x ∈ I) (hy : y ∈ I) : ∃ (a : ℝ) (b : ℝ), a < x ∧ a < y ∧ x < b ∧ y < b ∧ Set.Icc a b ⊆ I

Two points of an open, order connected set lie strictly inside a closed interval still contained in the set.

theorem CIV.continuousOn_primitive_of_isOpen {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {τ₀ : ℝ} (hτ₀ : τ₀ ∈ I) {h : ℝ → ℝ} (hh : MeasureTheory.LocallyIntegrableOn h I MeasureTheory.volume) : ContinuousOn (fun (τ : ℝ) => ∫ (s : ℝ) in τ₀..τ, h s) I

The primitive τ ↦ ∫ s in τ₀..τ, h s of a function locally integrable on an open, order connected I is continuous on I.

theorem CIV.continuous_mul_of_continuousOn_hasCompactSupport {I : Set ℝ} (hI : IsOpen I) {k ψ : ℝ → ℝ} (hk : ContinuousOn k I) (hψ : Continuous ψ) (hψI : tsupport ψ ⊆ I) : Continuous fun (x : ℝ) => k x * ψ x

The product of a function continuous on an open I with a globally continuous function whose support lies in I is continuous, once extended by zero.

theorem CIV.integrable_mul_of_continuousOn_hasCompactSupport {I : Set ℝ} (hI : IsOpen I) {k ψ : ℝ → ℝ} (hk : ContinuousOn k I) (hψ : Continuous ψ) (hψcs : HasCompactSupport ψ) (hψI : tsupport ψ ⊆ I) : MeasureTheory.Integrable (fun (x : ℝ) => k x * ψ x) MeasureTheory.volume

The product of a function continuous on an open I with a smooth compactly supported function whose support lies in I is integrable.

theorem CIV.tsupport_sub_subset (f g : ℝ → ℝ) : tsupport (f - g) ⊆ tsupport f ∪ tsupport g

A function vanishing off the topological support of another has that support inside it, once the ambient set is closed.

theorem CIV.eq_add_intervalIntegral_of_pairing_eq {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {f h : ℝ → ℝ} (hfc : ContinuousOn f I) (hh : MeasureTheory.LocallyIntegrableOn h I MeasureTheory.volume) (hDist : ∀ (χ : ℝ → ℝ), ContDiff ℝ (↑⊤) χ → HasCompactSupport χ → tsupport χ ⊆ I → ∫ (τ : ℝ), f τ * -deriv χ τ = ∫ (τ : ℝ), χ τ * h τ) {τ₀ : ℝ} (hτ₀ : τ₀ ∈ I) {τ : ℝ} (hτ : τ ∈ I) : f τ = f τ₀ + ∫ (s : ℝ) in τ₀..τ, h s

The distributional fundamental theorem of calculus: if f is continuous on an open, order connected I, h is locally integrable on I, and f obeys the tested identity ∫ f (-χ') = ∫ χ h for every smooth compactly supported χ with support in I (the shape mollified_equation delivers), then f is literally the primitive of h based at any τ₀ ∈ I, throughout I.