The comparison assertions from the transfer of essential bounds

This file reduces both assertions of lem:aniso:comparison, the statements CIV.comparison and CIV.comparisonAncient, to one transfer property of essential bounds forward in time: for a.e. reference time τ₀ and a.e. later time τ, every essential bound M of q (·, τ₀) is an essential bound of q (·, τ). This is the hypothesis hstep, in the binder shape of comparison_eLpNorm_top_of_ae_dominance, which converts it into the eLpNorm ⊤ conclusion. Both theorems below take every hypothesis of the corresponding statement, plus hstep, and have exactly its conclusion.

The transfer property itself is proved from the hypotheses of the comparison lemma by CIV.ae_ae_abs_le_of_isDistributionalDriftDiffusion; CIV.Main.comparisonAncient combines it with comparisonAncient_of_eLpNorm_transfer. Every function constant in time satisfies hstep (hstep_of_forall_eq_of_time_indep).

The hypotheses hd, hI, hB and heq of comparison_of_eLpNorm_transfer are not used by its proof, which goes through hq and hstep alone; they are kept, under their ordinary names, so that its hypotheses are those of the statement.

theorem CIV.hstep_of_forall_eq_of_time_indep {m : ℕ} {I : Set ℝ} {q : CKN.Vec m × ℝ → ℝ} (hconst : ∀ (x : CKN.Vec m) (τ τ' : ℝ), q (x, τ) = q (x, τ')) : ∀ᵐ (τ₀ : ℝ) (τ : ℝ) ∂MeasureTheory.volume.restrict I, τ₀ < τ → ∀ (M : ℝ), (∀ᵐ (x : CKN.Vec m), |q (x, τ₀)| ≤ M) → ∀ᵐ (x : CKN.Vec m), |q (x, τ)| ≤ M

hstep is satisfiable. Any function constant in the time variable satisfies the transfer hypothesis hstep of comparison_of_eLpNorm_transfer: the bounding condition at a reference time τ₀ and at a later time τ are then literally the same statement, since q (·, τ) and q (·, τ₀) agree pointwise for every x. In particular every steady state satisfies hstep.

theorem CIV.comparison_of_eLpNorm_transfer (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) (hstep : ∀ᵐ (τ₀ : ℝ) (τ : ℝ) ∂MeasureTheory.volume.restrict I, τ₀ < τ → ∀ (M : ℝ), (∀ᵐ (x : CKN.Vec m), |q (x, τ₀)| ≤ M) → ∀ᵐ (x : CKN.Vec m), |q (x, τ)| ≤ M) : ∀ᵐ (τ₀ : ℝ) (τ : ℝ) ∂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

comparison, from the transfer of essential bounds. Every hypothesis of the statement CIV.comparison is carried unchanged; the one addition is hstep, the transfer hypothesis of comparison_eLpNorm_top_of_ae_dominance, in that lemma's binder shape. The conclusion is that of CIV.comparison.

hd, hI, hB and heq are not used by this derivation, which goes through hq and hstep alone: given hstep, comparison_eLpNorm_top_of_ae_dominance supplies the eLpNorm ⊤ reformulation, and nothing further is needed from the drift or distributional hypotheses. The transfer property hstep follows from hI, hB, hq and heq by CIV.ae_ae_abs_le_of_isDistributionalDriftDiffusion.

theorem CIV.comparisonAncient_of_eLpNorm_transfer (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 * |τ| ^ (-κ))) (hstep : ∀ᵐ (τ₀ : ℝ) (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Iio T), τ₀ < τ → ∀ (M : ℝ), (∀ᵐ (x : CKN.Vec m), |q (x, τ₀)| ≤ M) → ∀ᵐ (x : CKN.Vec m), |q (x, τ)| ≤ M) : (∀ᵐ (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

comparisonAncient, from the transfer of essential bounds. Every hypothesis of the statement CIV.comparisonAncient is carried unchanged; the one addition is hstep, in the same shape as comparison_of_eLpNorm_transfer above, instantiated at I := Iio T. The conclusion is that of CIV.comparisonAncient.

The proof composes three lemmas. comparison_of_eLpNorm_transfer supplies, from hstep, exactly the comparison-monotonicity hypothesis ancientVanishing_ae_eq_zero needs. ancientVanishing_ae_eq_zero then proves the first conjunct from that and the decay hypothesis hdecay. ancientVanishing_continuousOn_eq_zero proves the second conjunct from the first; it is stated over V, q', openness, continuity and the a.e. agreement in the shape of the statement.