The drift hypotheses of the finite-axis limit equation

The lifted drift B_n = (V_n X/R, W_n) of eq:drift:Bn:def and its divergence div_{X,Z} B_n = 2 V_n / R (continued to the axis by 2 ∂_R V_n), at the moving axis points (0, z_n) of eq:aniso:zoom:finite:variables, have the three properties from which the admissible limiting drift of eq:aniso:zoom:finite:limit is extracted:

• continuity on every compact subset of ℝ⁵ × (-∞, -1], for all large n;
• for every compact set of times in (-∞, -1], one constant bounding B_n, div B_n and their spatial Lipschitz constants on every ball, for all large n (the footnote to eq:drift:Bn:def);
• on every time slice, div B_n is the weak divergence of B_n (div_{X,Z} B_n = 2 V_n/R off the axis, the axis being a null set crossed by a Lipschitz field).

theorem CIV.continuousOn_prod_of_lipschitz_of_continuousOn {E : Type u_1} [SeminormedAddCommGroup E] (F : CKN.Vec 5 × ℝ → E) (A : Set (CKN.Vec 5)) (J : Set ℝ) (L : ℝ) (hlip : ∀ τ ∈ J, ∀ x ∈ A, ∀ y ∈ A, ‖F (x, τ) - F (y, τ)‖ ≤ L * ‖x - y‖) (htime : ∀ x ∈ A, ContinuousOn (fun (τ : ℝ) => F (x, τ)) J) : ContinuousOn F (A ×ˢ J)

A function Lipschitz in space, uniformly in time, and continuous in time at every point, is jointly continuous.

theorem CIV.continuousOn_time_zoomDrift_finDriftDiv {lam h zc : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (x : CKN.Vec 5) (J : Set ℝ) (hJ : ∀ τ ∈ J, zoomPoint lam h zc (zoomLiftPoint (x, τ)) ∈ unitCylinder) : ContinuousOn (fun (τ : ℝ) => zoomDrift lam h zc u (x, τ)) J ∧ ContinuousOn (fun (τ : ℝ) => finDriftDiv lam h zc u (x, τ)) J

The lifted drift and divergence are continuous in time at a fixed lifted point, on a set of times at which the zoomed point stays in the cylinder.

theorem CIV.eventually_forall_rect_zoomPoint_mem {h ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) {zc : ℕ → ℝ} (hzc : ∀ (n : ℕ), |zc n| ≤ ρ) {lam : ℕ → ℝ} (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (r : ℝ) (J : Set ℝ) (hJ : IsCompact J) (hJt : ∀ τ ∈ J, τ ≤ -1) : ∀ᶠ (n : ℕ) in Filter.atTop, (0 < lam n ∧ lam n < 1 ∧ lam n ^ (2 * h) ≤ 1) ∧ ∀ τ ∈ J, ∀ y ∈ Set.Icc 0 (2 * r) ×ˢ Set.Icc (-r) r, zoomPoint (lam n) h (zc n) (y, τ) ∈ unitCylinder

For every radius and compact set of times in (-∞, -1], eventually the zoom maps the rectangle [0, 2r] × [-r, r] into the cylinder at every such time.

theorem CIV.finDrift_uniform_lipschitz {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))) (J : Set ℝ) : IsCompact J → J ⊆ Set.Iic (-1) → ∃ (Λ : ℝ), ∀ (r : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, ∀ x ∈ Metric.closedBall 0 r, ∀ y ∈ Metric.closedBall 0 r, ‖zoomDrift (lam n) h (zc n) u (x, τ)‖ ≤ Λ ∧ |finDriftDiv (lam n) h (zc n) u (x, τ)| ≤ Λ ∧ ‖zoomDrift (lam n) h (zc n) u (x, τ) - zoomDrift (lam n) h (zc n) u (y, τ)‖ ≤ Λ * ‖x - y‖ ∧ |finDriftDiv (lam n) h (zc n) u (x, τ) - finDriftDiv (lam n) h (zc n) u (y, τ)| ≤ Λ * ‖x - y‖

The uniform bounds and Lipschitz bounds of the lifted drift and divergence on every ball.

theorem CIV.finDrift_eventually_continuousOn {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.Iic (-1) → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (zoomDrift (lam n) h (zc n) u) K ∧ ContinuousOn (finDriftDiv (lam n) h (zc n) u) K

The lifted drift and divergence are eventually continuous on every compact subset of ℝ⁵ × (-∞, -1].

theorem CIV.add_smul_basisVec_eq_update (x : CKN.Vec 5) (i : Fin 5) (t : ℝ) : x + t • CKN.basisVec i = Function.update x i (x i + t)

x + t e_i is x with its i-th coordinate moved by t.

theorem CIV.norm_lineDeriv_le_of_lipschitzWith {g : CKN.Vec 5 → ℝ} {Λ : NNReal} (hg : LipschitzWith Λ g) (x v : CKN.Vec 5) : ‖lineDeriv ℝ g x v‖ ≤ ↑Λ * ‖v‖

The line derivative of a function bounded by the Lipschitz constant times ‖v‖.

theorem CIV.integral_finDriftDiv_mul_eq {C h lam zc r tau : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pr f unitCylinder) (hb : AnisotropicBounds C h u) (haxi : IsAxisymmetricOn u unitCylinder) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h ≤ 1 / 2) (htau : tau ≤ -1) (hmem : ∀ y ∈ Set.Icc 0 (2 * r) ×ˢ Set.Icc (-r) r, zoomPoint lam h zc (y, tau) ∈ unitCylinder) (ψ : CKN.Vec 5 → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψr : tsupport ψ ⊆ Metric.ball 0 r) : ∫ (x : CKN.Vec 5), finDriftDiv lam h zc u (x, tau) * ψ x = -∫ (x : CKN.Vec 5), ∑ i : Fin 5, zoomDrift lam h zc u (x, tau) i * (fderiv ℝ ψ x) (CKN.basisVec i)

On one time slice, div B_n = 2 V_n / R is the weak divergence of the lifted drift. The drift is Lipschitz across the axis (norm_zoomDrift_sub_le), so Rademacher's integration by parts applies to (a Lipschitz extension of) each component, and its classical divergence off the null axis is 2 V_n / R (zoomDriftDivergence_eq).

theorem CIV.finDrift_extraction_hypotheses {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) {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pr f 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.Iic (-1) → ∀ᶠ (n : ℕ) in Filter.atTop, ContinuousOn (zoomDrift (lam n) h (zc n) u) K ∧ ContinuousOn (finDriftDiv (lam n) h (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, ‖zoomDrift (lam n) h (zc n) u (x, τ)‖ ≤ Λ ∧ |finDriftDiv (lam n) h (zc n) u (x, τ)| ≤ Λ ∧ ‖zoomDrift (lam n) h (zc n) u (x, τ) - zoomDrift (lam n) h (zc n) u (y, τ)‖ ≤ Λ * ‖x - y‖ ∧ |finDriftDiv (lam n) h (zc n) u (x, τ) - finDriftDiv (lam n) h (zc n) u (y, τ)| ≤ Λ * ‖x - y‖) ∧ ∀ (ψ : CKN.Vec 5 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ (J : Set ℝ), IsCompact J → J ⊆ Set.Iic (-1) → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ τ ∈ J, ∫ (x : CKN.Vec 5), finDriftDiv (lam n) h (zc n) u (x, τ) * ψ x = -∫ (x : CKN.Vec 5), ∑ i : Fin 5, zoomDrift (lam n) h (zc n) u (x, τ) i * (fderiv ℝ ψ x) (CKN.basisVec i)

F2-H: the three hypotheses of the drift extraction for the lifted finite-axis drift at the moving axis points: eventual continuity on compacts, uniform bounds and Lipschitz bounds on every ball, and the slice weak divergence.