Ancient Vanishing

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

theorem CIV.ancientVanishing_ae_eq_zero {m : ℕ} {T : ℝ} {q : CKN.Vec m × ℝ → ℝ} (hq : IsLocallyBoundedOn m (Set.Iio T) 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 * |τ| ^ (-κ))) (hcomp : ∀ᵐ (τ₀ : ℝ) (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Iio T), τ₀ < τ → MeasureTheory.eLpNorm (fun (x : CKN.Vec m) => q (x, τ)) ⊤ MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : CKN.Vec m) => q (x, τ₀)) ⊤ MeasureTheory.volume) : ∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Iio T), q z = 0

Ancient vanishing, first conjunct of CIV.comparisonAncient. Given the comparison monotonicity conclusion (the L^∞ norm of a later slice is bounded by an earlier one, almost everywhere) together with the stated L^∞ decay as the reference time recedes to -∞, q vanishes almost everywhere on Vec m × Iio T.

theorem CIV.ancientVanishing_continuousOn_eq_zero {m : ℕ} {T : ℝ} {q : CKN.Vec m × ℝ → ℝ} (hzero : ∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Iio T), q z = 0) {V : Set (CKN.Vec m × ℝ)} {q' : CKN.Vec m × ℝ → ℝ} (hV : IsOpen V) (hcont : ContinuousOn q' (V ∩ Set.univ ×ˢ Set.Iic T)) (heqOn : ∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict (V ∩ Set.univ ×ˢ Set.Iio T), q' z = q z) (z : CKN.Vec m × ℝ) : z ∈ V ∩ Set.univ ×ˢ Set.Iic T → q' z = 0

Ancient vanishing, second conjunct of CIV.comparisonAncient. Given that q vanishes almost everywhere on univ ×ˢ Iio T, any continuous representative q' on V ∩ univ ×ˢ Iic T that agrees with q almost everywhere on the open set V ∩ univ ×ˢ Iio T vanishes at every point of the closed set V ∩ univ ×ˢ Iic T: the open set is dense in the closed one (every point with τ = T is a limit of points with τ < T), so the almost-everywhere vanishing upgrades to everywhere vanishing by continuity, including at the endpoint τ = T.