Reference times of the mollified equation, in both Fubini orders

For each spatial point x, the mollified slice q_ε(x, ·) satisfies the primitive identity of eq:aniso:comparison:mollified between almost every pair of times (CIV.mollifySlice_ae_ae_sub_eq_intervalIntegral). The comparison argument anchors the identity at a reference time τ₀ and needs it, from that anchor, both for almost every x along almost every later time, and for almost every later time at almost every x. This file proves that almost every τ₀ ∈ I is such an anchor, by crossing the per-point statement into a statement on the triple product Vec m × I × I (as CIV.mollifySlice_ae_prod_sub_eq_intervalIntegral does) and reading it off in both orders.

The set of anchors depends on q (it is defined through q's own slices), which is the manuscript's choice of a reference time of q: a function obtained from q by redefining one slice has a different set of anchors.

noncomputable def CIV.mollifiedRHS (m d : ℕ) (ε : ℝ) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB q : CKN.Vec m × ℝ → ℝ) (x : CKN.Vec m) (s : ℝ) : ℝ

The right side of eq:aniso:comparison:mollified at the point (x, s).

Equations

• One or more equations did not get rendered due to their size.

theorem CIV.setIntegral_restrict_eq_of_subset {g : ℝ → ℝ} {S I : Set ℝ} (hI : MeasurableSet I) (hSI : S ⊆ I) : ∫ (s : ℝ) in S, g s ∂MeasureTheory.volume.restrict I = ∫ (s : ℝ) in S, g s

theorem CIV.intervalIntegral_restrict_eq_of_mem {g : ℝ → ℝ} {I : Set ℝ} (hI : IsOpen I) (hIoc : I.OrdConnected) {τ1 τ2 : ℝ} (hτ1 : τ1 ∈ I) (hτ2 : τ2 ∈ I) : ∫ (s : ℝ) in τ1..τ2, g s ∂MeasureTheory.volume.restrict I = ∫ (s : ℝ) in τ1..τ2, g s

theorem CIV.mollifySlice_sub_eq_intervalIntegral_ae_prod {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 < ε) {τ₀ : ℝ} (hτ₀ : τ₀ ∈ I) : ∀ᵐ (p : CKN.Vec m × ℝ × ℝ) ∂MeasureTheory.volume.prod ((MeasureTheory.volume.restrict I).prod (MeasureTheory.volume.restrict I)), mollifySlice m ε q (p.1, p.2.2) - mollifySlice m ε q (p.1, p.2.1) = ∫ (s : ℝ) in p.2.1..p.2.2, mollifiedRHS m d ε B divB q p.1 s

The primitive identity of the mollified equation holds almost everywhere on the triple product Vec m × I × I.

theorem CIV.ae_isReferenceTime_mollifySlice {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) {εs : ℕ → ℝ} (hεs : ∀ (n : ℕ), 0 < εs n) : ∀ᵐ (τ₀ : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (n : ℕ), (∀ᵐ (x : CKN.Vec m), ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict I, mollifySlice m (εs n) q (x, τ) - mollifySlice m (εs n) q (x, τ₀) = ∫ (s : ℝ) in τ₀..τ, mollifiedRHS m d (εs n) B divB q x s) ∧ ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict I, ∀ᵐ (x : CKN.Vec m), mollifySlice m (εs n) q (x, τ) - mollifySlice m (εs n) q (x, τ₀) = ∫ (s : ℝ) in τ₀..τ, mollifiedRHS m d (εs n) B divB q x s

Almost every τ₀ ∈ I is a reference time of the mollified equation in both Fubini orders, simultaneously for every ε of a given sequence of positive mollification radii.