The public statement CIV.Main.comparisonAncient

This module proves the statement CIV.comparisonAncient, the last assertion of lem:aniso:comparison. The transfer of essential bounds forward in time (CIV.ae_ae_abs_le_of_isDistributionalDriftDiffusion, on I = (-∞, T)) is applied at times where the decay eq:aniso:ancient:decay holds and which tend to -∞ (CIV.comparisonAncient_of_eLpNorm_transfer).

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

The public statement of lem:aniso:comparison, ancient assertion with the decay eq:aniso:ancient:decay.