The comparison principle applied to the two ancient limits of prop:aniso:small

The last step of each branch of the zoom argument of prop:aniso:small applies the last assertion of lem:aniso:comparison to the limiting scalar:

• in the finite-axis case, to the lifted limit Ω_∞(X, Z, τ) = Ω(|X|, Z, τ) of the rescaled potential vorticities on ℝ⁴ × ℝ × (-∞, -1), with (m, d) = (5, 4) and κ = 3/2 + h (the paragraph after eq:aniso:zoom:finite:limit);
• in the receding-axis case, to the limit Θ of the rescaled azimuthal vorticities on ℝ² × (-∞, -1), with (m, d) = (2, 1) and κ = 1 + h (the paragraph after eq:aniso:zoom:receding:limit).

In both cases the limit is continuous on the relevant open set up to the endpoint τ = -1 (it is a locally uniform limit) and obeys the decay bound inherited from eq:aniso:zoom:finite:bound or eq:aniso:zoom:receding:bound. The two theorems below take exactly these facts, together with the admissible drift and the distributional limit equation, and conclude that the limit vanishes at every point of {τ = -1} (off the axis in the finite-axis case). The local boundedness, the measurability and the decay premise of the comparison lemma are derived here from the continuity and the pointwise bound; the axis {X = 0} of the lifted variables is a null set.

The axis of the lifted variables is a null set

theorem CIV.volume_zoomLiftAxis_eq_zero : MeasureTheory.volume {z : CKN.Vec 5 × ℝ | zoomLiftRadius z.1 = 0} = 0

The axis {X = 0} of the lifted variables Vec 5 × ℝ is contained in the null hyperplane {X₀ = 0}.

theorem CIV.ae_zoomLiftRadius_pos (μ : MeasureTheory.Measure (CKN.Vec 5 × ℝ)) (hμ : μ.AbsolutelyContinuous MeasureTheory.volume) : ∀ᵐ (z : CKN.Vec 5 × ℝ) ∂μ, 0 < zoomLiftRadius z.1

Almost every lifted point lies off the axis.

theorem CIV.ae_zoomLiftRadius_pos_vec : ∀ᵐ (x : CKN.Vec 5), 0 < zoomLiftRadius x

Almost every lifted spatial point lies off the axis.

theorem CIV.continuous_zoomLiftPoint : Continuous zoomLiftPoint

zoomLiftPoint is continuous.

The finite-axis case, (m, d) = (5, 4)

theorem CIV.zoomLiftPoint_mk {R Z τ : ℝ} (hR : 0 ≤ R) : zoomLiftPoint (![R, 0, 0, 0, Z], τ) = ((R, Z), τ)

The point (R, 0, 0, 0, Z) of the lifted space lies at lifted radius R ≥ 0 and height Z.

theorem CIV.isLocallyBoundedOn_zoomLift {C h : ℝ} (hh : 0 < h) (Ω : (ℝ × ℝ) × ℝ → ℝ) (hΩc : ContinuousOn Ω {p : (ℝ × ℝ) × ℝ | 0 < p.1.1 ∧ p.2 ≤ -1}) (hΩb : ∀ (p : (ℝ × ℝ) × ℝ), 0 < p.1.1 → p.2 ≤ -1 → |Ω p| ≤ C * (-p.2) ^ (-(3 / 2) - h)) : IsLocallyBoundedOn 5 (Set.Iio (-1)) fun (z : CKN.Vec 5 × ℝ) => Ω (zoomLiftPoint z)

The lift of a function continuous on {R > 0, τ ≤ -1} and bounded there by C |τ|^{-3/2-h} is locally bounded on ℝ⁵ × (-∞, -1) (the axis is a null set).

theorem CIV.zoomOmegaLimit_endpoint_eq_zero {C h : ℝ} (hh : 0 < h) (Ω : (ℝ × ℝ) × ℝ → ℝ) (hΩc : ContinuousOn Ω {p : (ℝ × ℝ) × ℝ | 0 < p.1.1 ∧ p.2 ≤ -1}) (hΩb : ∀ (p : (ℝ × ℝ) × ℝ), 0 < p.1.1 → p.2 ≤ -1 → |Ω p| ≤ C * (-p.2) ^ (-(3 / 2) - h)) (B : CKN.Vec 5 × ℝ → CKN.Vec 5) (divB : CKN.Vec 5 × ℝ → ℝ) (hB : IsAdmissibleDrift 5 (Set.Iio (-1)) B divB) (heq : IsDistributionalDriftDiffusion 5 4 (Set.Iio (-1)) B divB fun (z : CKN.Vec 5 × ℝ) => Ω (zoomLiftPoint z)) (p : ℝ × ℝ) : 0 < p.1 → Ω (p, -1) = 0

The comparison principle applied to the finite-axis limit (the paragraph after eq:aniso:zoom:finite:limit): a function Ω of ((R, Z), τ), continuous on {R > 0, τ ≤ -1} and bounded there by C |τ|^{-3/2-h}, whose lift to ℝ⁴ × ℝ solves the limit equation eq:aniso:zoom:finite:limit in the sense of distributions on (-∞, -1) with an admissible drift, vanishes at every point (R, Z, -1) with R > 0. This is the last assertion of lem:aniso:comparison with (m, d) = (5, 4) and κ = 3/2 + h.

The receding-axis case, (m, d) = (2, 1)

def CIV.planeLiftPoint (z : CKN.Vec 2 × ℝ) : (ℝ × ℝ) × ℝ

The meridional point ((R, Z), τ) read from a point of Vec 2 × ℝ.

Equations

• CIV.planeLiftPoint z = ((z.1 0, z.1 1), z.2)

theorem CIV.continuous_planeLiftPoint : Continuous planeLiftPoint

planeLiftPoint is continuous.

theorem CIV.zoomThetaLimit_endpoint_eq_zero {C h : ℝ} (hh : 0 < h) (Θ : (ℝ × ℝ) × ℝ → ℝ) (hΘc : ContinuousOn Θ {p : (ℝ × ℝ) × ℝ | p.2 ≤ -1}) (hΘb : ∀ (p : (ℝ × ℝ) × ℝ), p.2 ≤ -1 → |Θ p| ≤ C * (-p.2) ^ (-1 - h)) (B : CKN.Vec 2 × ℝ → CKN.Vec 2) (divB : CKN.Vec 2 × ℝ → ℝ) (hB : IsAdmissibleDrift 2 (Set.Iio (-1)) B divB) (heq : IsDistributionalDriftDiffusion 2 1 (Set.Iio (-1)) B divB fun (z : CKN.Vec 2 × ℝ) => Θ (planeLiftPoint z)) (p : ℝ × ℝ) : Θ (p, -1) = 0

The comparison principle applied to the receding-axis limit (the paragraph after eq:aniso:zoom:receding:limit): a function Θ of ((R, Z), τ), continuous on {τ ≤ -1} and bounded there by C |τ|^{-1-h}, which solves the limit equation eq:aniso:zoom:receding:limit:a in the sense of distributions on ℝ² × (-∞, -1) with an admissible drift and diffusion in R alone, vanishes at every point (R, Z, -1). This is the last assertion of lem:aniso:comparison with (m, d) = (2, 1) and κ = 1 + h.