The public statement CIV.Main.comparison

This module proves the statement CIV.comparison, the first assertion of lem:aniso:comparison, eq:aniso:comparison:conclusion. The proof is CIV.comparison_of_isDistributionalDriftDiffusion: mollify in space, compare the mollified solution with the barrier eq:aniso:comparison:barrier through the energy of eq:aniso:comparison:positive:energy from a reference time of the mollified equation, let the mollification radius and then the barrier slope tend to zero, and exhaust I by compact intervals. The hypothesis 1 ≤ d ≤ m of the statement is not used: for d = 0 the equation has no diffusion and the argument applies verbatim, and for d > m the partial Laplacian is the full Laplacian.

theorem CIV.Main.comparison (m d : ℕ) (hd : 1 ≤ d ∧ d ≤ m) (I : Set ℝ) (hI : IsOpen I ∧ I.OrdConnected) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB : CKN.Vec m × ℝ → ℝ) (hB : IsAdmissibleDrift m I B divB) (q : CKN.Vec m × ℝ → ℝ) (hq : IsLocallyBoundedOn m I q) (heq : IsDistributionalDriftDiffusion m d I B divB q) : ∀ᵐ (τ₀ : ℝ) (τ : ℝ) ∂MeasureTheory.volume.restrict I, τ₀ < τ → MeasureTheory.eLpNorm (fun (x : CKN.Vec m) => q (x, τ)) ⊤ MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : CKN.Vec m) => q (x, τ₀)) ⊤ MeasureTheory.volume

The public statement of lem:aniso:comparison, first assertion.