Comparison

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.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

Lemma 3.3 (lem:aniso:comparison), first assertion.