The energy at almost every time is a time integral from the reference time

Fix a reference time τ₀ of the mollified equation (CIV.ae_isReferenceTime_mollifySlice) at which the mollified slice lies below M. For each spatial point x, the function L(x, τ) = q_ε(x, τ₀) + ∫_{τ₀}^τ H(x, r) dr is absolutely continuous in τ and agrees with q_ε(x, τ) at almost every τ for almost every x (this is the time representative of the manuscript, the sentence after eq:aniso:comparison:mollified); at τ₀ it is the mollified slice itself. The chain rule for the comparison profile G along L - Ψ_σ then gives, for almost every later time τ and almost every x,

G(q_ε(x, τ) - Ψ_σ(x, τ)) = ∫_{τ₀}^τ G'(q_ε - Ψ_σ)(x, s) (H(x, s) - ∂_τΨ_σ) ds,

since G(q_ε - Ψ_σ) vanishes at τ₀.

theorem CIV.barrier_time_shift {m : ℕ} (M σ K τ₀ s : ℝ) (x : CKN.Vec m) : barrier m M σ K τ₀ (x, s) = barrier m M σ K τ₀ (x, τ₀) + σ * K * (s - τ₀)

theorem CIV.le_barrier_at_anchor {m : ℕ} (M K τ₀ : ℝ) {σ : ℝ} (hσ : 0 ≤ σ) (x : CKN.Vec m) : M ≤ barrier m M σ K τ₀ (x, τ₀)

theorem CIV.intervalIntegrable_mollifiedRHS {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) (hτ₂ : τ₂ ∈ I) : IntervalIntegrable (fun (s : ℝ) => mollifiedRHS m d ε B divB q x s) MeasureTheory.volume τ₁ τ₂

The time integrability of the right side of the mollified equation at a fixed point.

theorem CIV.comparisonProfile_representative_eq {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 < ε) {M σ K τ₀ τ : ℝ} (hσ : 0 ≤ σ) (hτ₀ : τ₀ ∈ I) (hτ : τ ∈ I) (x : CKN.Vec m) (hq0 : mollifySlice m ε q (x, τ₀) ≤ M) (hx : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, mollifySlice m ε q (x, s) - mollifySlice m ε q (x, τ₀) = ∫ (r : ℝ) in τ₀..s, mollifiedRHS m d ε B divB q x r) : comparisonProfile ((mollifySlice m ε q (x, τ₀) + ∫ (r : ℝ) in τ₀..τ, mollifiedRHS m d ε B divB q x r) - barrier m M σ K τ₀ (x, τ)) = ∫ (s : ℝ) in τ₀..τ, (mollifySlice m ε q (x, s) - barrier m M σ K τ₀ (x, s)).smoothTransition * (mollifiedRHS m d ε B divB q x s - σ * K)

The energy density along the time representative, at one spatial point.

theorem CIV.ae_ae_comparisonProfile_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 < ε) {M σ K τ₀ : ℝ} (hσ : 0 ≤ σ) (hτ₀ : τ₀ ∈ I) (hq0 : ∀ (x : CKN.Vec m), mollifySlice m ε q (x, τ₀) ≤ M) (hA1 : ∀ᵐ (x : CKN.Vec m), ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict I, mollifySlice m ε q (x, τ) - mollifySlice m ε q (x, τ₀) = ∫ (s : ℝ) in τ₀..τ, mollifiedRHS m d ε B divB q x s) (hA2 : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict I, ∀ᵐ (x : CKN.Vec m), mollifySlice m ε q (x, τ) - mollifySlice m ε q (x, τ₀) = ∫ (s : ℝ) in τ₀..τ, mollifiedRHS m d ε B divB q x s) : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict I, ∀ᵐ (x : CKN.Vec m), comparisonProfile (mollifySlice m ε q (x, τ) - barrier m M σ K τ₀ (x, τ)) = ∫ (s : ℝ) in τ₀..τ, (mollifySlice m ε q (x, s) - barrier m M σ K τ₀ (x, s)).smoothTransition * (mollifiedRHS m d ε B divB q x s - σ * K)

The energy density at almost every later time, for almost every point, is the time integral from the reference time τ₀ of G'(q_ε - Ψ_σ)(H - ∂_τΨ_σ).