The receding-branch drift and its continuity, boundedness, and measurability inputs

At the receding zoom centre x_n = (r_n, z_n) of the proof of prop:aniso:small (eq:aniso:zoom:receding:variables), this file packages the meridional drift (V_n, W_n) and its divergence eq:aniso:zoom:receding:div as a genuine drift pair on Vec 2 × ℝ, and proves the eventual continuity/Lipschitz/weak-divergence inputs and the eventual measurability/boundedness inputs that the extraction of an admissible drift limit (CIV.exists_subseq_admissibleDrift) needs at this branch, at the moving zoom centre (rc n, zc n) with r_n / λ_n → ∞.

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

The receding drift (V_n, W_n) on Vec 2 × ℝ, lifted from the meridional plane.

Equations

• CIV.recDrift lam h rc zc u z = ![CIV.zoomVRec lam h rc zc u (CIV.planeLiftPoint z), CIV.zoomWRec lam h rc zc u (CIV.planeLiftPoint z)]

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

Its divergence ∂_R V_n + ∂_Z W_n = -V_n / (A_n + R) (eq:aniso:zoom:receding:div).

Equations

• CIV.recDriftDiv lam h rc zc u z = -(CIV.zoomVRec lam h rc zc u (CIV.planeLiftPoint z) / (rc / lam + z.1 0))

Enclosing a compact subset of Vec 2 × ℝ in a plane-and-time box

R2-B: bounds and measurability of the receding sequences

theorem CIV.recDrift_bounds {h ρ Rstar C : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρR : ρ < Rstar) (hR1 : Rstar ≤ 1) {rc zc : ℕ → ℝ} (hcz : ∀ (n : ℕ), rc n ^ 2 + zc n ^ 2 ≤ ρ ^ 2) (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) {lam : ℕ → ℝ} (hlam_pos : ∀ (n : ℕ), 0 < lam n) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (hA : Filter.Tendsto (fun (n : ℕ) => rc n / lam n) Filter.atTop Filter.atTop) (K : Set (CKN.Vec 2 × ℝ)) : IsCompact K → K ⊆ Set.univ ×ˢ Set.Iio (-1) → ∃ (M : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Vec 2 × ℝ) => zoomTheta (lam n) h (rc n) (zc n) u (planeLiftPoint z)) (MeasureTheory.volume.restrict K) ∧ MeasureTheory.AEStronglyMeasurable (recDrift (lam n) h (rc n) (zc n) u) (MeasureTheory.volume.restrict K) ∧ MeasureTheory.AEStronglyMeasurable (recDriftDiv (lam n) h (rc n) (zc n) u) (MeasureTheory.volume.restrict K) ∧ ∀ z ∈ K, |zoomTheta (lam n) h (rc n) (zc n) u (planeLiftPoint z)| ≤ M ∧ ‖recDrift (lam n) h (rc n) (zc n) u z‖ ≤ M ∧ |recDriftDiv (lam n) h (rc n) (zc n) u z| ≤ M

R2-B: local bounds and measurability of the receding sequences Θ_n, (V_n, W_n), and the divergence -V_n / (A_n + R), at the moving zoom centre (rc n, zc n).

R2-H: continuity, Lipschitz bound, and weak divergence of the receding drift

The coordinate bridge between Vec 2 calculus and the plane operators dr, dz

theorem CIV.recDrift_extraction_hypotheses {h ρ Rstar C : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρR : ρ < Rstar) (hR1 : Rstar ≤ 1) {rc zc : ℕ → ℝ} (hcz : ∀ (n : ℕ), rc n ^ 2 + zc n ^ 2 ≤ ρ ^ 2) (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) {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {lam : ℕ → ℝ} (hlam_pos : ∀ (n : ℕ), 0 < lam n) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (hA : Filter.Tendsto (fun (n : ℕ) => rc n / lam n) Filter.atTop Filter.atTop) : (∀ (K : Set (CKN.Vec 2 × ℝ)), IsCompact K → K ⊆ Set.univ ×ˢ Set.Iic (-1) → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (recDrift (lam n) h (rc n) (zc n) u) K ∧ ContinuousOn (recDriftDiv (lam n) h (rc n) (zc n) u) K) ∧ (∀ (J : Set ℝ), IsCompact J → J ⊆ Set.Iic (-1) → ∃ (Λ : ℝ), ∀ (r : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, ∀ x ∈ Metric.closedBall 0 r, ∀ y ∈ Metric.closedBall 0 r, ‖recDrift (lam n) h (rc n) (zc n) u (x, τ)‖ ≤ Λ ∧ |recDriftDiv (lam n) h (rc n) (zc n) u (x, τ)| ≤ Λ ∧ ‖recDrift (lam n) h (rc n) (zc n) u (x, τ) - recDrift (lam n) h (rc n) (zc n) u (y, τ)‖ ≤ Λ * ‖x - y‖ ∧ |recDriftDiv (lam n) h (rc n) (zc n) u (x, τ) - recDriftDiv (lam n) h (rc n) (zc n) u (y, τ)| ≤ Λ * ‖x - y‖) ∧ ∀ (ψ : CKN.Vec 2 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ (J : Set ℝ), IsCompact J → J ⊆ Set.Iic (-1) → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, ∫ (x : CKN.Vec 2), recDriftDiv (lam n) h (rc n) (zc n) u (x, τ) * ψ x = -∫ (x : CKN.Vec 2), ∑ i : Fin 2, recDrift (lam n) h (rc n) (zc n) u (x, τ) i * (fderiv ℝ ψ x) (CKN.basisVec i)

R2-H: the hypotheses of G-DRIFT at the receding zoom fields.