The Grönwall bound for the comparison energy at fixed mollification

This is eq:aniso:comparison:positive:energy integrated in time, followed by Grönwall's inequality, at a fixed mollification radius ε and barrier slope σ. On a working interval [τ₀, b] ⊆ I starting at a reference time τ₀ of the mollified equation at which the mollified slice lies below M, the energy E(τ) = ∫ G(q_ε(x, τ) - Ψ_σ(x, τ)) dx satisfies, for almost every τ ∈ [τ₀, b] and every δ > 0,

E(τ) ≤ (δ |B_R| (b - τ₀) + (4δ)⁻¹ ∫_{τ₀}^b ‖R_ε(s)‖²_{L²(B_R)} ds) e^{Λ (b - τ₀)},

with R = Mq / σ the radius outside which the excess is negative. The δ-splitting |R_ε| ≤ δ + R_ε² / (4δ) replaces the Cauchy–Schwarz step of the manuscript and leads to the same conclusion as ε ↓ 0 (the commutator term tends to zero, CIV.tendsto_integral_commutatorL2Sq).

The time regularity used is exactly the one the manuscript's representative provides: the energy agrees at almost every time with the primitive P(τ) = ∫_{τ₀}^τ ∫ G'(w)(H - ∂_τΨ_σ) dx ds (CIV.ae_ae_comparisonProfile_eq_intervalIntegral and Fubini), and Grönwall is applied to the continuous function P.

theorem CIV.exists_measurableSet_subset_forall_of_ae {J : Set ℝ} (hJ : MeasurableSet J) {P : ℝ → Prop} (h : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, P s) : ∃ (T : Set ℝ), MeasurableSet T ∧ T ⊆ J ∧ (∀ s ∈ T, P s) ∧ MeasureTheory.volume (J \ T) = 0

A property holding almost everywhere on a measurable set holds on a measurable subset of full measure.

theorem CIV.abs_le_add_sq_div {δ : ℝ} (hδ : 0 < δ) (r : ℝ) : |r| ≤ δ + r ^ 2 / (4 * δ)

theorem CIV.integral_mul_abs_le_of_support {m : ℕ} {f R : CKN.Vec m → ℝ} {ρ δ Cr : ℝ} (hδ : 0 < δ) (hf0 : ∀ (x : CKN.Vec m), 0 ≤ f x) (hf1 : ∀ (x : CKN.Vec m), f x ≤ 1) (hfs : ∀ x ∉ Metric.closedBall 0 ρ, f x = 0) (hRm : MeasureTheory.AEStronglyMeasurable R MeasureTheory.volume) (hRb : ∀ᵐ (x : CKN.Vec m), |R x| ≤ Cr) : ∫ (x : CKN.Vec m), f x * |R x| ≤ δ * (MeasureTheory.volume (Metric.closedBall 0 ρ)).toReal + 1 / (4 * δ) * ∫ (x : CKN.Vec m) in Metric.closedBall 0 ρ, R x ^ 2

The δ-splitting of the commutator term against a weight with values in [0, 1] supported in a closed ball.