The lifted finite-axis equation off the axis

Off the axis X = 0, the lifted potential vorticity Ω_tilde_n = Ω_n ∘ L of eq:aniso:zoom:lifted, with L(X, Z, τ) = (|X|, Z, τ), is smooth and satisfies pointwise ∂_τ Ω_tilde_n + B_n · ∇Ω_tilde_n = Δ_X Ω_tilde_n + δ_n² ∂_ZZ Ω_tilde_n + ∂_Z F_tilde_n + G_tilde_n, where B_n is the drift of eq:drift:Bn:def, F_n = S_n² / R² is the swirl flux and G_n the force term of eq:aniso:zoom:finite:equation (finLift_pde); the divergence of B_n there is 2 V_n / R = finDriftDiv (finLift_div). This is the lift to ℝ⁴: the radial operator ∂_RR + 3 R⁻¹ ∂_R is the Laplacian of ℝ⁴ acting on the lift. Integrating by parts (integral_liftedResidual_eq) turns the equation into the identity integral_finResidual_eq_of_subset_finLiftDomain for test functions supported off the axis.

def CIV.finMeridionalDomain (lam h zc : ℝ) : Set ((ℝ × ℝ) × ℝ)

The open set of meridional points off the axis whose zoomed image lies in the unit cylinder.

Equations

• CIV.finMeridionalDomain lam h zc = {p : (ℝ × ℝ) × ℝ | 0 < p.1.1 ∧ CIV.zoomPoint lam h zc p ∈ CIV.unitCylinder}

theorem CIV.isOpen_finMeridionalDomain (lam h zc : ℝ) : IsOpen (finMeridionalDomain lam h zc)

theorem CIV.zoomLiftPoint_mem_finMeridionalDomain {lam h zc : ℝ} {z : CKN.Vec 5 × ℝ} (hz : z ∈ finLiftDomain lam h zc) : zoomLiftPoint z ∈ finMeridionalDomain lam h zc

The lift maps the off-axis lifted domain into the off-axis meridional domain.

theorem CIV.contDiffOn_potentialVorticity_zoomPoint {lam h zc : ℝ} (hlam : 0 < lam) {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hv : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v z) unitCylinder) : ContDiffOn ℝ (↑⊤) (fun (p : (ℝ × ℝ) × ℝ) => potentialVorticity v (zoomPoint lam h zc p)) (finMeridionalDomain lam h zc)

The potential vorticity of a smooth field, read through the zoom map, is smooth off the axis.

theorem CIV.contDiffOn_component_zoomPoint {lam h zc : ℝ} {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hv : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v z) unitCylinder) (k : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (p : (ℝ × ℝ) × ℝ) => v (zoomPoint lam h zc p) k) (finMeridionalDomain lam h zc)

A component of a smooth field, read through the zoom map, is smooth off the axis.

theorem CIV.contDiffOn_zoomOmega_finMeridional {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) : ContDiffOn ℝ (↑⊤) (zoomOmega lam h zc u) (finMeridionalDomain lam h zc)

theorem CIV.contDiffOn_zoomForce_finMeridional {lam h zc : ℝ} (hlam : 0 < lam) {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) : ContDiffOn ℝ (↑⊤) (zoomForce lam h zc f) (finMeridionalDomain lam h zc)

theorem CIV.contDiffOn_zoomV_finMeridional {lam h zc : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContDiffOn ℝ (↑⊤) (zoomV lam h zc u) (finMeridionalDomain lam h zc)

theorem CIV.contDiffOn_zoomW_finMeridional {lam h zc : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContDiffOn ℝ (↑⊤) (zoomW lam h zc u) (finMeridionalDomain lam h zc)

theorem CIV.contDiffOn_zoomSwirlFlux_finMeridional {lam h zc : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContDiffOn ℝ (↑⊤) (fun (q : (ℝ × ℝ) × ℝ) => zoomS lam h zc u q ^ 2 / q.1.1 ^ 2) (finMeridionalDomain lam h zc)

The swirl flux S_n² / R² is smooth off the axis.

theorem CIV.contDiffOn_comp_zoomLiftPoint {lam h zc : ℝ} {g : (ℝ × ℝ) × ℝ → ℝ} (hg : ContDiffOn ℝ (↑⊤) g (finMeridionalDomain lam h zc)) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Vec 5 × ℝ) => g (zoomLiftPoint z)) (finLiftDomain lam h zc)

A function smooth off the axis in the meridional variables lifts to a function smooth off the axis in the lifted variables.

theorem CIV.differentiableAt_of_finLiftDomain {lam h zc : ℝ} {g : (ℝ × ℝ) × ℝ → ℝ} (hg : ContDiffOn ℝ (↑⊤) g (finMeridionalDomain lam h zc)) {z : CKN.Vec 5 × ℝ} (hz : z ∈ finLiftDomain lam h zc) : DifferentiableAt ℝ g (zoomLiftPoint z)

A function smooth off the axis is differentiable at the lift of an off-axis point.

theorem CIV.zoomDrift_apply_fun_of_ne (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) {i : Fin 5} (hi : i ≠ 4) : (fun (w : CKN.Vec 5 × ℝ) => zoomDrift lam h zc u w i) = fun (w : CKN.Vec 5 × ℝ) => zoomV lam h zc u (zoomLiftPoint w) * (w.1 i / zoomLiftRadius w.1)

The radial components of the lifted drift, as functions.

theorem CIV.zoomDrift_apply_fun_four (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : (fun (w : CKN.Vec 5 × ℝ) => zoomDrift lam h zc u w 4) = fun (w : CKN.Vec 5 × ℝ) => zoomW lam h zc u (zoomLiftPoint w)

The vertical component of the lifted drift, as a function.

theorem CIV.contDiffOn_zoomDrift_apply {lam h zc : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (i : Fin 5) : ContDiffOn ℝ (↑⊤) (fun (w : CKN.Vec 5 × ℝ) => zoomDrift lam h zc u w i) (finLiftDomain lam h zc)

The components of the lifted drift are smooth off the axis.

theorem CIV.sum_sq_eq_zoomLiftRadius_sq (X : CKN.Vec 5) : X 0 ^ 2 + X 1 ^ 2 + X 2 ^ 2 + X 3 ^ 2 = zoomLiftRadius X ^ 2

The four squared radial coordinates sum to the squared lifted radius.

theorem CIV.sum_radial_lift_identities {X : CKN.Vec 5} (hR : 0 < zoomLiftRadius X) : (X 0 / zoomLiftRadius X) ^ 2 + (X 1 / zoomLiftRadius X) ^ 2 + (X 2 / zoomLiftRadius X) ^ 2 + (X 3 / zoomLiftRadius X) ^ 2 = 1 ∧ 1 / zoomLiftRadius X - X 0 ^ 2 / zoomLiftRadius X ^ 3 + (1 / zoomLiftRadius X - X 1 ^ 2 / zoomLiftRadius X ^ 3) + (1 / zoomLiftRadius X - X 2 ^ 2 / zoomLiftRadius X ^ 3) + (1 / zoomLiftRadius X - X 3 ^ 2 / zoomLiftRadius X ^ 3) = 3 / zoomLiftRadius X

The two radial sums produced by the lift.

theorem CIV.finLift_div {lam h zc : ℝ} (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) (haxi : IsAxisymmetricOn u unitCylinder) {z : CKN.Vec 5 × ℝ} (hz : z ∈ finLiftDomain lam h zc) : ∑ i : Fin 5, (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => zoomDrift lam h zc u w i) z) (CKN.basisVec i, 0) = finDriftDiv lam h zc u z

The divergence of the lifted drift off the axis is 2 V_n / R.

theorem CIV.zoomOmegaLift_eq_fun (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : zoomOmegaLift lam h zc u = fun (w : CKN.Vec 5 × ℝ) => zoomOmega lam h zc u (zoomLiftPoint w)

The lifted potential vorticity is the lift of zoomOmega.

theorem CIV.finLift_pde {lam h zc : ℝ} (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) (haxi : IsAxisymmetricOn u unitCylinder) {z : CKN.Vec 5 × ℝ} (hz : z ∈ finLiftDomain lam h zc) : (fderiv ℝ (zoomOmegaLift lam h zc u) z) (0, 1) + ∑ i : Fin 5, zoomDrift lam h zc u z i * (fderiv ℝ (zoomOmegaLift lam h zc u) z) (CKN.basisVec i, 0) = (∑ i : Fin 5, if ↑i < 4 then (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => (fderiv ℝ (zoomOmegaLift lam h zc u) w) (CKN.basisVec i, 0)) z) (CKN.basisVec i, 0) else 0) + (lam ^ (2 * h)) ^ 2 * (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => (fderiv ℝ (zoomOmegaLift lam h zc u) w) (CKN.basisVec 4, 0)) z) (CKN.basisVec 4, 0) + (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => zoomS lam h zc u (zoomLiftPoint w) ^ 2 / (zoomLiftPoint w).1.1 ^ 2) z) (CKN.basisVec 4, 0) + zoomForce lam h zc f (zoomLiftPoint z)

The lifted equation eq:aniso:zoom:lifted off the axis: the lift to ℝ⁴ applied to eq:aniso:zoom:finite:equation.

theorem CIV.integral_finResidual_eq_of_subset_finLiftDomain {lam h zc : ℝ} (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) (haxi : IsAxisymmetricOn u unitCylinder) {K : Set (CKN.Vec 5 × ℝ)} (hK : IsCompact K) (hKS : K ⊆ finLiftDomain lam h zc) {ψ : CKN.Vec 5 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψK : tsupport ψ ⊆ K) : ∫ (z : CKN.Vec 5 × ℝ), zoomOmegaLift lam h zc u z * (-timeDeriv 5 ψ z - gradPair 5 ψ z (zoomDrift lam h zc u z) - finDriftDiv lam h zc u z * ψ z - partialLaplacian 5 4 ψ z) = ∫ (z : CKN.Vec 5 × ℝ), (lam ^ (2 * h)) ^ 2 * zoomOmegaLift lam h zc u z * (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => (fderiv ℝ ψ w) (CKN.basisVec 4, 0)) z) (CKN.basisVec 4, 0) - zoomS lam h zc u (zoomLiftPoint z) ^ 2 / (zoomLiftPoint z).1.1 ^ 2 * (fderiv ℝ ψ z) (CKN.basisVec 4, 0) + zoomForce lam h zc f (zoomLiftPoint z) * ψ z

The residual identity off the axis: against a test function supported in a compact subset of the off-axis lifted domain, the pairing of Ω_tilde_n with the adjoint operator of eq:aniso:zoom:finite:limit equals δ_n² ∫ Ω_tilde_n ∂_ZZ ψ - ∫ F_tilde_n ∂_Z ψ + ∫ G_tilde_n ψ.