The finite-n residual of the lifted equation tends to zero

tendsto_finResidual is the input of the finite branch to the limit equation eq:aniso:zoom:finite:limit at (m, d) = (5, 4) (the lift to ℝ⁴ together with the vanishing terms of the passage to the limit, deviation D17): against a test function φ on ℝ⁴ × ℝ × (-∞, -1), the pairing of the lifted potential vorticity Ω_tilde_n with the adjoint limit operator -∂_τ φ - B_n · ∇φ - (div B_n) φ - Δ_X φ tends to zero.

The test function is split with the axis cutoff finAxisCutoff ε as φ = φ χ_ε + φ (1 - χ_ε).

• Near the axis, Ω_tilde_n, B_n and div B_n are bounded uniformly in n (finDrift_bounds), the derivatives of φ χ_ε of order at most two are O(ε⁻²), and the support has volume O(ε⁴): this part is O(ε²) uniformly in n (abs_integral_residual_nearAxis_le).
• Off the axis, the lifted equation holds classically and the integration by parts of integral_finResidual_eq_of_subset_finLiftDomain leaves `δ_n² ∫ Ω_tilde_n ∂_ZZ ψ - ∫ F_tilde_n ∂_Z ψ
  • ∫ G_tilde_n ψ. Here |Ω_tilde_n| ≤ 2C, the swirl flux obeys F_n = S_n² / R² ≤ C_Γ² δ_n² / ε⁴by `eq:aniso:zoom:circulation, and |G_n| ≤ C λ_n⁵ δ_n; all three tend to zero with λ_n (tendsto_integral_residual_offAxis`).

theorem CIV.abs_integral_le_of_forall_notMem {S : Set (CKN.Vec 5 × ℝ)} (hS : MeasureTheory.volume S < ⊤) {g : CKN.Vec 5 × ℝ → ℝ} {Q : ℝ} (h0 : ∀ z ∉ S, g z = 0) (hQ : ∀ z ∈ S, |g z| ≤ Q) : |∫ (z : CKN.Vec 5 × ℝ), g z| ≤ Q * (MeasureTheory.volume S).toReal

A function vanishing off a measurable set of finite measure and bounded on it has integral bounded by the bound times the measure.

theorem CIV.volume_axisBox (ε r : ℝ) (hε : 0 ≤ ε) (hr : 0 ≤ r) : (MeasureTheory.volume ((Set.univ.pi fun (j : Fin 5) => Set.Icc (-if j = 4 then r else 2 * ε) (if j = 4 then r else 2 * ε)) ×ˢ Set.Icc (-r) r)).toReal = (4 * ε) ^ 4 * (2 * r) * (2 * r)

The box {|X_j| ≤ 2ε, |Z| ≤ r, |τ| ≤ r} around the axis of the lifted variables.

theorem CIV.tsupport_finAxisCutoff_subset (ε : ℝ) : tsupport (finAxisCutoff ε) ⊆ {z : CKN.Vec 5 × ℝ | ‖(ε⁻¹ • finAxisProj) z‖ ≤ 2}

The support of the cutoff lies where the rescaled radial part has norm at most two.

theorem CIV.abs_integral_residual_nearAxis_le {K : Set (CKN.Vec 5 × ℝ)} {r : ℝ} (hr : 0 ≤ r) (hKr : ∀ z ∈ K, ‖z‖ ≤ r) {q d : CKN.Vec 5 × ℝ → ℝ} {b : CKN.Vec 5 × ℝ → CKN.Vec 5} {M : ℝ} (hM : 0 ≤ M) (hbd : ∀ z ∈ K, |q z| ≤ M ∧ ‖b z‖ ≤ M ∧ |d z| ≤ M) {φ : CKN.Vec 5 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφK : tsupport φ ⊆ K) {A : ℝ} (hA : ∀ j ≤ 2, ∀ (z : CKN.Vec 5 × ℝ), ‖iteratedFDeriv ℝ j φ z‖ ≤ A) {Cb : ℝ} (hCb : ∀ j ≤ 2, ∀ (y : CKN.Vec 5), ‖iteratedFDeriv ℝ j (↑finAxisBump) y‖ ≤ Cb) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : |∫ (z : CKN.Vec 5 × ℝ), q z * (-timeDeriv 5 (fun (y : CKN.Vec 5 × ℝ) => φ y * finAxisCutoff ε y) z - gradPair 5 (fun (y : CKN.Vec 5 × ℝ) => φ y * finAxisCutoff ε y) z (b z) - d z * (φ z * finAxisCutoff ε z) - partialLaplacian 5 4 (fun (y : CKN.Vec 5 × ℝ) => φ y * finAxisCutoff ε y) z)| ≤ M * (2 * M + 5) * (4 * (A * (Cb * ε⁻¹ ^ 2))) * ((4 * ε) ^ 4 * (2 * r) * (2 * r))

The part of the residual near the axis is O(ε²), uniformly in the coefficients as long as they are bounded by M on the support.

theorem CIV.abs_fderiv_apply_basisVec_le {ψ : CKN.Vec 5 × ℝ → ℝ} (z : CKN.Vec 5 × ℝ) (i : Fin 5) : |(fderiv ℝ ψ z) (CKN.basisVec i, 0)| ≤ ‖iteratedFDeriv ℝ 1 ψ z‖

A first derivative in a coordinate direction is bounded by the first derivative.

theorem CIV.abs_fderiv_fderiv_apply_basisVec_le {ψ : CKN.Vec 5 × ℝ → ℝ} (hψ : ContDiff ℝ 2 ψ) (z : CKN.Vec 5 × ℝ) (i : Fin 5) : |(fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => (fderiv ℝ ψ w) (CKN.basisVec i, 0)) z) (CKN.basisVec i, 0)| ≤ ‖iteratedFDeriv ℝ 2 ψ z‖

A second derivative in a coordinate direction is bounded by the second derivative.

theorem CIV.tsupport_one_sub_finAxisCutoff_subset (ε : ℝ) : (tsupport fun (y : CKN.Vec 5 × ℝ) => 1 - finAxisCutoff ε y) ⊆ {z : CKN.Vec 5 × ℝ | 1 ≤ ‖(ε⁻¹ • finAxisProj) z‖}

The support of 1 - χ_ε lies where the rescaled radial part has norm at least one.

theorem CIV.abs_zoomSwirlFlux_le {lam h zc CΓ ε : ℝ} (hlam : 0 < lam) (hε : 0 < ε) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : (ℝ × ℝ) × ℝ} (hR : ε ≤ p.1.1) (hΓ : |circulation u (zoomPoint lam h zc p)| ≤ CΓ) : |zoomS lam h zc u p ^ 2 / p.1.1 ^ 2| ≤ CΓ ^ 2 * (lam ^ (2 * h)) ^ 2 / ε ^ 4

The swirl flux off the axis: S_n² / R² ≤ C_Γ² δ² / ε⁴ where R ≥ ε and the circulation is bounded by C_Γ (eq:aniso:zoom:circulation).

theorem CIV.tendsto_integral_residual_offAxis {C h CΓ ρ Rstar tstar : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {lam zc : ℕ → ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρR : ρ < Rstar) (hR1 : Rstar ≤ 1) (htstar : tstar < 0) (hzc : ∀ (n : ℕ), |zc n| ≤ ρ) (hC : 0 ≤ C) (hb : AnisotropicBounds C h u) (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (hΓ : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∀ t ∈ Set.Ioo tstar 0, |circulation u (x, t)| ≤ CΓ) (hforce : ForceC2Bounded f) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) {φ : CKN.Vec 5 × ℝ → ℝ} (hφ : φ ∈ testFunctions 5 (Set.Iio (-1))) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec 5 × ℝ), zoomOmegaLift (lam n) h (zc n) u z * (-timeDeriv 5 (fun (y : CKN.Vec 5 × ℝ) => φ y * (1 - finAxisCutoff ε y)) z - gradPair 5 (fun (y : CKN.Vec 5 × ℝ) => φ y * (1 - finAxisCutoff ε y)) z (zoomDrift (lam n) h (zc n) u z) - finDriftDiv (lam n) h (zc n) u z * (φ z * (1 - finAxisCutoff ε z)) - partialLaplacian 5 4 (fun (y : CKN.Vec 5 × ℝ) => φ y * (1 - finAxisCutoff ε y)) z)) Filter.atTop (nhds 0)

The part of the residual off the axis tends to zero, for each fixed cutoff scale ε.

theorem CIV.tendsto_finResidual {C h CΓ ρ Rstar tstar : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {lam zc : ℕ → ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρR : ρ < Rstar) (hR1 : Rstar ≤ 1) (htstar : tstar < 0) (hzc : ∀ (n : ℕ), |zc n| ≤ ρ) (hC : 0 ≤ C) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (hΓ : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∀ t ∈ Set.Ioo tstar 0, |circulation u (x, t)| ≤ CΓ) (hforce : ForceC2Bounded f) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) (φ : CKN.Vec 5 × ℝ → ℝ) : φ ∈ testFunctions 5 (Set.Iio (-1)) → Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Vec 5 × ℝ), zoomOmegaLift (lam n) h (zc n) u z * (-timeDeriv 5 φ z - gradPair 5 φ z (zoomDrift (lam n) h (zc n) u z) - finDriftDiv (lam n) h (zc n) u z * φ z - partialLaplacian 5 4 φ z)) Filter.atTop (nhds 0)

The lift to ℝ⁴ and the vanishing terms of the passage to the limit: the finite-n residual of eq:aniso:zoom:lifted against a test function on ℝ⁴ × ℝ × (-∞, -1) tends to zero.