The lifted finite-axis fields: divergence, bounds and measurability

In Step 2 of the proof of prop:aniso:small the rescaled potential vorticity Ω_n and the drift B_n = (V_n X/R, W_n) of eq:drift:Bn:def are regarded as functions on ℝ⁴ × ℝ × (-∞, -1] (eq:aniso:zoom:lifted). The divergence of the drift is div_{X,Z} B_n = 2 V_n / R, continued to the axis by 2 ∂_R V_n (finDriftDiv). On a compact set of the lifted variables with τ < -1, for all large n, the three fields are almost everywhere continuous (the axis is a null set) and bounded by a constant independent of n, by eq:aniso:zoom:finite:bound and eq:aniso:zoom:derivatives.

noncomputable def CIV.finDriftDiv (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Vec 5 × ℝ) : ℝ

The lifted divergence div_{X,Z} B_n = 2 V_n / R, continued to the axis by 2 ∂_R V_n.

Equations

• One or more equations did not get rendered due to their size.

theorem CIV.continuous_zoomPoint_zoomLiftPoint (lam h zc : ℝ) : Continuous fun (z : CKN.Vec 5 × ℝ) => zoomPoint lam h zc (zoomLiftPoint z)

The zoom map composed with the lift is continuous.

theorem CIV.zoomLiftRadius_continuous : Continuous zoomLiftRadius

def CIV.finLiftDomain (lam h zc : ℝ) : Set (CKN.Vec 5 × ℝ)

The off-axis part of the lifted preimage of the unit cylinder.

Equations

• CIV.finLiftDomain lam h zc = {z : CKN.Vec 5 × ℝ | 0 < CIV.zoomLiftRadius z.1 ∧ CIV.zoomPoint lam h zc (CIV.zoomLiftPoint z) ∈ CIV.unitCylinder}

theorem CIV.isOpen_finLiftDomain (lam h zc : ℝ) : IsOpen (finLiftDomain lam h zc)

theorem CIV.continuousOn_finLift_fields {lam h zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContinuousOn (zoomOmegaLift lam h zc u) (finLiftDomain lam h zc) ∧ ContinuousOn (zoomDrift lam h zc u) (finLiftDomain lam h zc) ∧ ContinuousOn (finDriftDiv lam h zc u) (finLiftDomain lam h zc)

The three lifted fields are continuous off the axis on the lifted preimage.

theorem CIV.ae_restrict_zoomLiftRadius_pos (K : Set (CKN.Vec 5 × ℝ)) : ∀ᵐ (z : CKN.Vec 5 × ℝ) ∂MeasureTheory.volume.restrict K, 0 < zoomLiftRadius z.1

Almost every lifted point of a set lies off the axis, for the restricted measure.

theorem CIV.aestronglyMeasurable_of_continuousOn_offAxis {E : Type u_1} [NormedAddCommGroup E] [SecondCountableTopology E] {g : CKN.Vec 5 × ℝ → E} {K : Set (CKN.Vec 5 × ℝ)} (hK : MeasurableSet K) (hg : ContinuousOn g (K ∩ {z : CKN.Vec 5 × ℝ | 0 < zoomLiftRadius z.1})) : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict K)

A function continuous on the off-axis part of a measurable set is almost everywhere strongly measurable for the restricted measure.

theorem CIV.finDrift_bounds {C h ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hC : 0 ≤ C) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {zc : ℕ → ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ρ) {lam : ℕ → ℝ} (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (K : Set (CKN.Vec 5 × ℝ)) : IsCompact K → K ⊆ Set.univ ×ˢ Set.Iio (-1) → ∃ (M : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.AEStronglyMeasurable (zoomOmegaLift (lam n) h (zc n) u) (MeasureTheory.volume.restrict K) ∧ MeasureTheory.AEStronglyMeasurable (zoomDrift (lam n) h (zc n) u) (MeasureTheory.volume.restrict K) ∧ MeasureTheory.AEStronglyMeasurable (finDriftDiv (lam n) h (zc n) u) (MeasureTheory.volume.restrict K) ∧ ∀ z ∈ K, |zoomOmegaLift (lam n) h (zc n) u z| ≤ M ∧ ‖zoomDrift (lam n) h (zc n) u z‖ ≤ M ∧ |finDriftDiv (lam n) h (zc n) u z| ≤ M

F2-B: on a compact set of the lifted variables with τ < -1, for all large n, the lifted scalar, drift and divergence are almost everywhere strongly measurable and bounded by 2C.

theorem CIV.tendsto_lintegral_zoomOmegaLift {C h ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hC : 0 ≤ C) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {zc : ℕ → ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ρ) {lam : ℕ → ℝ} (hlam_pos : ∀ (n : ℕ), 0 < lam n) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (Ω : (ℝ × ℝ) × ℝ → ℝ) (hconv : ∀ (K : Set ((ℝ × ℝ) × ℝ)), IsCompact K → K ⊆ {p : (ℝ × ℝ) × ℝ | 0 < p.1.1 ∧ p.2 ≤ -1} → TendstoUniformlyOn (fun (n : ℕ) => zoomOmega (lam n) h (zc n) u) Ω Filter.atTop K) (K : Set (CKN.Vec 5 × ℝ)) : IsCompact K → K ⊆ Set.univ ×ˢ Set.Iio (-1) → Filter.Tendsto (fun (n : ℕ) => ∫⁻ (z : CKN.Vec 5 × ℝ) in K, ‖zoomOmegaLift (lam n) h (zc n) u z - Ω (zoomLiftPoint z)‖ₑ) Filter.atTop (nhds 0)

F2-S (eq:aniso:zoom:finite:strong): if the rescaled potential vorticities converge uniformly on compact subsets of {R > 0, τ ≤ -1}, their lifts converge in L¹ on every compact subset of ℝ⁵ × (-∞, -1): off a thin tube around the axis the convergence is uniform, and the tube, on which both sides stay bounded, has small measure.