Comparison Ancient

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

theorem CIV.comparisonAncient (m d : ℕ) (hd : 1 ≤ d ∧ d ≤ m) (T : ℝ) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB : CKN.Vec m × ℝ → ℝ) (hB : IsAdmissibleDrift m (Set.Iio T) B divB) (q : CKN.Vec m × ℝ → ℝ) (hq : IsLocallyBoundedOn m (Set.Iio T) q) (heq : IsDistributionalDriftDiffusion m d (Set.Iio T) B divB q) (C κ : ℝ) (hκ : 0 < κ) (hdecay : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Iio (min (-1) T)), MeasureTheory.eLpNorm (fun (x : CKN.Vec m) => q (x, τ)) ⊤ MeasureTheory.volume ≤ ENNReal.ofReal (C * |τ| ^ (-κ))) : (∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Iio T), q z = 0) ∧ ∀ (V : Set (CKN.Vec m × ℝ)) (q' : CKN.Vec m × ℝ → ℝ), IsOpen V → ContinuousOn q' (V ∩ Set.univ ×ˢ Set.Iic T) → (∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict (V ∩ Set.univ ×ˢ Set.Iio T), q' z = q z) → ∀ z ∈ V ∩ Set.univ ×ˢ Set.Iic T, q' z = 0

Lemma 3.3 (lem:aniso:comparison), ancient assertion with the decay eq:aniso:ancient:decay.