The representative lemma: an a.e. fundamental theorem of calculus, unconditional in x

CIV/Comparison/EnergyInequality2.lean proves the distributional fundamental theorem of calculus eq_add_intervalIntegral_of_pairing_eq: a function f continuous on an open, order-connected I, paired against every smooth compactly supported test function the same way a locally integrable h is, equals a primitive of h throughout I. Applying that theorem to f = mollifySlice m ε q (x, ·) — the shape mollified_equation supplies the pairing for — needs two extra facts at the fixed spatial point x: continuity of the slice in time (hCont), and local integrability in time of the right side of eq:aniso:comparison:mollified (hLoc). Neither follows from the hypotheses of the comparison lemma (IsAdmissibleDrift, IsLocallyBoundedOn, IsDistributionalDriftDiffusion): a two-function counterexample differing only on the null slice Vec m × {0} gives mollified slices at τ = 0 that differ, so hCont is a genuine restriction on the chosen representative of q, not a consequence of those hypotheses.

This file dispenses with both hypotheses by weakening the conclusion from "holds everywhere on I" to "holds for a.e. τ₁, τ₂ ∈ I" wherever they are needed:

• ae_ae_sub_eq_intervalIntegral_of_pairing_eq is the a.e. weakening of eq_add_intervalIntegral_of_pairing_eq: hfc : ContinuousOn f I is replaced by hfLoc : LocallyIntegrableOn f I volume, and the conclusion becomes the difference identity f τ₂ - f τ₁ = ∫ s in τ₁..τ₂, h s, holding for a.e. τ₁ ∈ I and (the same null set) a.e. τ₂ ∈ I. Continuity enters the proof of the everywhere version only to promote the a.e.-constant conclusion of the abstract du Bois-Reymond argument (ae_eq_zero_of_integral_contDiff_smul_eq_zero) to an everywhere statement, and to supply integrability side conditions; dropping the promotion and re-deriving the side conditions from local integrability removes the need for it. Working with the difference rather than an absolute primitive additionally removes the unknown integration constant: it cancels between any two points where the a.e. identity holds.

• locallyIntegrableOn_mollifySlice and locallyIntegrableOn_mollifiedRHS supply the two local integrability facts the a.e. lemma needs, unconditionally in x, directly from the hypotheses hB, hq, heq, hε of the comparison lemma, with no hCont/hLoc hypothesis. The second is the substantial one: it repeats, at a smooth bump function centred at each point of I, exactly the integrability computation already carried out inside the proof of mollified_equation for whichever single test function that theorem is handed.

• mollifySlice_ae_ae_sub_eq_intervalIntegral combines the three: for every x, a.e. τ₁ ∈ I and a.e. τ₂ ∈ I, mollifySlice m ε q (x, τ₂) - mollifySlice m ε q (x, τ₁) equals the interval integral of the right side of eq:aniso:comparison:mollified. Compared with CIV.mollifySlice_eq_add_intervalIntegral, the same conclusion (as a difference, a.e. rather than everywhere) follows from hB, hq, heq, hε alone.

Scope

The identity is proved for each fixed x, and the exceptional null set of pairs (τ₁, τ₂) may depend on x. The joint statement, almost everywhere on Vec m × I × I, is CIV.mollifySlice_sub_eq_intervalIntegral_ae_prod; the comparison proof uses it to choose a reference time (CIV.ae_isReferenceTime_mollifySlice).

Part 0: local helpers

theorem CIV.integrable_mul_of_locallyIntegrableOn_hasCompactSupport {I : Set ℝ} {f ψ : ℝ → ℝ} (hf : MeasureTheory.LocallyIntegrableOn f I MeasureTheory.volume) (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) (hψI : tsupport ψ ⊆ I) : MeasureTheory.Integrable (fun (τ : ℝ) => f τ * ψ τ) MeasureTheory.volume

The product of a function locally integrable on an open I with a continuous, compactly supported function whose support lies in I is integrable, with no continuity hypothesis on the first factor. This is the local-integrability replacement for EnergyInequality2.integrable_mul_of_continuousOn_hasCompactSupport.

theorem CIV.exists_bump_eq_one_near_of_isOpen {I : Set ℝ} (hI : IsOpen I) {τ₀ : ℝ} (hτ₀ : τ₀ ∈ I) : ∃ (χ : ℝ → ℝ), ContDiff ℝ (↑⊤) χ ∧ HasCompactSupport χ ∧ tsupport χ ⊆ I ∧ ∃ (r : ℝ), 0 < r ∧ ∀ τ ∈ Metric.closedBall τ₀ r, χ τ = 1

A smooth, compactly supported bump function centred at a point of an open set I, with support inside I and equal to 1 on a smaller closed ball around the centre.

theorem CIV.integrableOn_closedBall_of_integrable_mul_bump {f χ : ℝ → ℝ} {τ₀ r : ℝ} (hone : ∀ τ ∈ Metric.closedBall τ₀ r, χ τ = 1) (hint : MeasureTheory.Integrable (fun (τ : ℝ) => f τ * χ τ) MeasureTheory.volume) : MeasureTheory.IntegrableOn f (Metric.closedBall τ₀ r) MeasureTheory.volume

If f multiplied by a bump function χ equal to 1 on closedBall τ₀ r is integrable, then f alone is integrable on that ball.

Part 1: the a.e. distributional fundamental theorem of calculus

theorem CIV.ae_ae_sub_eq_intervalIntegral_of_pairing_eq {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {f h : ℝ → ℝ} (hfLoc : MeasureTheory.LocallyIntegrableOn f I MeasureTheory.volume) (hh : MeasureTheory.LocallyIntegrableOn h I MeasureTheory.volume) (hDist : ∀ (χ : ℝ → ℝ), ContDiff ℝ (↑⊤) χ → HasCompactSupport χ → tsupport χ ⊆ I → ∫ (τ : ℝ), f τ * -deriv χ τ = ∫ (τ : ℝ), χ τ * h τ) {τ₀ : ℝ} (hτ₀ : τ₀ ∈ I) : ∀ᵐ (τ₁ : ℝ) (τ₂ : ℝ) ∂MeasureTheory.volume.restrict I, f τ₂ - f τ₁ = ∫ (s : ℝ) in τ₁..τ₂, h s

The a.e. weakening of eq_add_intervalIntegral_of_pairing_eq: replacing continuity of f on I by mere local integrability, and reading off the difference f τ₂ - f τ₁ instead of an absolute primitive (which removes the unknown integration constant, since it cancels), the same pairing hypothesis gives the fundamental-theorem-of-calculus identity for a.e. τ₁ ∈ I and a.e. τ₂ ∈ I.

Part 2: local integrability of the mollified slice, unconditional in x

theorem CIV.locallyIntegrableOn_mollifySlice {m : ℕ} {ε : ℝ} (hε : 0 < ε) (x : CKN.Vec m) {I : Set ℝ} (hI : IsOpen I) {q : CKN.Vec m × ℝ → ℝ} (hq : IsLocallyBoundedOn m I q) : MeasureTheory.LocallyIntegrableOn (fun (τ : ℝ) => mollifySlice m ε q (x, τ)) I MeasureTheory.volume

The mollified slice mollifySlice m ε q (x, ·) is locally integrable in time on I, for every spatial point x, from hq : IsLocallyBoundedOn alone.

Part 3: local integrability of the mollified right side, unconditional in x

theorem CIV.locallyIntegrableOn_mollifiedRHS {m d : ℕ} {ε : ℝ} (hε : 0 < ε) (x : CKN.Vec m) {I : Set ℝ} (hI : IsOpen I) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hq : IsLocallyBoundedOn m I q) (heq : IsDistributionalDriftDiffusion m d I B divB q) : MeasureTheory.LocallyIntegrableOn (fun (τ : ℝ) => partialLaplacian m d (mollifySlice m ε q) (x, τ) - gradPair m (mollifySlice m ε q) (x, τ) (B (x, τ)) + diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, τ)) (fun (y : CKN.Vec m) => divB (y, τ)) (fun (y : CKN.Vec m) => q (y, τ)) x) I MeasureTheory.volume

For every spatial point x, the right side of eq:aniso:comparison:mollified is locally integrable in time on I, directly from the hypotheses hB, hq, heq of the comparison lemma, with no hLoc hypothesis. The proof repeats, at a bump function centred at each point of I, exactly the integrability computation the proof of mollified_equation performs for whichever single test function that theorem is handed.

Part 4: the representative lemma

theorem CIV.mollifySlice_ae_ae_sub_eq_intervalIntegral {m d : ℕ} {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} (hB : IsAdmissibleDrift m I B divB) (hq : IsLocallyBoundedOn m I q) (heq : IsDistributionalDriftDiffusion m d I B divB q) {ε : ℝ} (hε : 0 < ε) (x : CKN.Vec m) {τ₀ : ℝ} (hτ₀ : τ₀ ∈ I) : ∀ᵐ (τ₁ : ℝ) (τ₂ : ℝ) ∂MeasureTheory.volume.restrict I, mollifySlice m ε q (x, τ₂) - mollifySlice m ε q (x, τ₁) = ∫ (s : ℝ) in τ₁..τ₂, partialLaplacian m d (mollifySlice m ε q) (x, s) - gradPair m (mollifySlice m ε q) (x, s) (B (x, s)) + diPernaLionsCommutator m ε (fun (y : CKN.Vec m) => B (y, s)) (fun (y : CKN.Vec m) => divB (y, s)) (fun (y : CKN.Vec m) => q (y, s)) x

The representative lemma. For every spatial point x and a.e. τ₁, τ₂ ∈ I, the mollified slice's change between τ₁ and τ₂ equals the interval integral of the right side of eq:aniso:comparison:mollified. This is the conclusion of CIV.mollifySlice_eq_add_intervalIntegral without its hypotheses hCont/hLoc, as an a.e. difference identity following from the hypotheses hB, hq, heq, hε of the comparison lemma alone.