The receding-axis zoom

The recentred zoom-in map of eq:aniso:zoom:receding:variables sends ((R, Z), τ) to the point with radius rc + lam * R, height zc + lam ^ (1 - 2 * h) * Z and parabolic time lam ^ 2 * τ. Only the radial slot differs from eq:aniso:zoom:finite:variables, and it differs by the constant offset rc, so every derivative in the recentred variables has exactly the same prefactor as in the finite-axis variables.

The file follows CIV.Zoom.Rescaling, CIV.Zoom.ChainRule, CIV.Zoom.ChainRuleSecond, CIV.Zoom.DivergenceIdentity and CIV.Zoom.RescaledBounds step by step; the receding declarations carry a Rec suffix so that the two families never clash. The second-derivative helpers are obtained from the general scalar chain rule of CIV.Zoom.ScalarChainRule, which is stated for an arbitrary curve inside a fixed time slice and therefore accepts the offset radial line of the recentred map.

The recentred zoom map and the rescaled fields

noncomputable def CIV.zoomPointRec (lam h rc zc : ℝ) (p : (ℝ × ℝ) × ℝ) : CKN.Foundation.Parabolic.ParabolicPoint

The recentred zoom-in map of eq:aniso:zoom:receding:variables, with the radial offset rc and the vertical offset zc.

Equations

• CIV.zoomPointRec lam h rc zc p = (CIV.meridional (rc + lam * p.1.1) (zc + lam ^ (1 - 2 * h) * p.1.2), lam ^ 2 * p.2)

noncomputable def CIV.zoomVRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

V_n of eq:aniso:zoom:fields in the recentred variables.

Equations

• CIV.zoomVRec lam h rc zc u p = lam * u (CIV.zoomPointRec lam h rc zc p) 0

noncomputable def CIV.zoomWRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

W_n of eq:aniso:zoom:fields in the recentred variables.

Equations

• CIV.zoomWRec lam h rc zc u p = lam * lam ^ (2 * h) * u (CIV.zoomPointRec lam h rc zc p) 2

noncomputable def CIV.zoomSRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

S_n of eq:aniso:zoom:fields in the recentred variables.

Equations

• CIV.zoomSRec lam h rc zc u p = lam * lam ^ (2 * h) * u (CIV.zoomPointRec lam h rc zc p) 1

noncomputable def CIV.zoomTheta (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

The rescaled azimuthal vorticity Θ_n = lam² δ_n ω_θ of eq:aniso:zoom:receding:vorticity.

Equations

• CIV.zoomTheta lam h rc zc u p = lam ^ 2 * lam ^ (2 * h) * CIV.azimuthalVorticity u (CIV.zoomPointRec lam h rc zc p)

Membership, continuity and smoothness of the recentred zoom map

theorem CIV.zoomPointRec_mem_unitCylinder_iff (lam h rc zc : ℝ) (p : (ℝ × ℝ) × ℝ) : zoomPointRec lam h rc zc p ∈ unitCylinder ↔ (rc + lam * p.1.1) ^ 2 + (zc + lam ^ (1 - 2 * h) * p.1.2) ^ 2 < 1 ∧ lam ^ 2 * p.2 ∈ Set.Ioo (-1) 0

Membership of the recentred zoom point in the unit cylinder, read off in coordinates. The time slot is lam ^ 2 * p.2 with p.2 = τ < 0, exactly as in zoomPoint_mem_unitCylinder_iff.

theorem CIV.continuous_zoomPointRec (lam h rc zc : ℝ) : Continuous fun (p : (ℝ × ℝ) × ℝ) => zoomPointRec lam h rc zc p

zoomPointRec is affine in p, hence continuous. As in continuous_zoomPoint, the codomain is named Y := Vec3 × ℝ so that the product topology, not the parabolic metric of ParabolicPoint, is the one used (design note R2).

theorem CIV.contDiff_zoomPointRec (lam h rc zc : ℝ) : ContDiff ℝ ↑⊤ fun (p : (ℝ × ℝ) × ℝ) => zoomPointRec lam h rc zc p

zoomPointRec is affine, hence smooth; the codomain is named F := Vec3 × ℝ for the same reason as in continuous_zoomPointRec.

Derivatives of the recentred meridional line

theorem CIV.hasDerivAt_meridional_fst_shift (b a c x : ℝ) : HasDerivAt (fun (s : ℝ) => meridional (b + a * s) c) (a • CKN.basisVec 0) x

Moving the radial coordinate of a meridional point away from the offset b at speed a moves it along e₁.

The recentred zoom map differentiated in R and in Z

theorem CIV.hasDerivAt_zoomRec_component_r (lam h rc zc : ℝ) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) (i : Fin 3) : HasDerivAt (fun (r : ℝ) => u (zoomPointRec lam h rc zc ((r, p.1.2), p.2)) i) (lam * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 0 (zoomPointRec lam h rc zc p)) p.1.1

Differentiating a component of u ∘ zoomPointRec in the radial variable.

theorem CIV.hasDerivAt_zoomRec_component_z (lam h rc zc : ℝ) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) (i : Fin 3) : HasDerivAt (fun (s : ℝ) => u (zoomPointRec lam h rc zc ((p.1.1, s), p.2)) i) (lam ^ (1 - 2 * h) * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 (zoomPointRec lam h rc zc p)) p.1.2

Differentiating a component of u ∘ zoomPointRec in the vertical variable.

First-order chain rules for the recentred fields

theorem CIV.dr_zoomVRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dr (zoomVRec lam h rc zc u) p = lam ^ 2 * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (zoomPointRec lam h rc zc p)

∂_R V_n in terms of the radial partial derivative of u_r.

theorem CIV.dz_zoomVRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dz (zoomVRec lam h rc zc u) p = lam * lam ^ (1 - 2 * h) * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 (zoomPointRec lam h rc zc p)

∂_Z V_n in terms of the vertical partial derivative of u_r.

theorem CIV.dr_zoomWRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dr (zoomWRec lam h rc zc u) p = lam ^ 2 * lam ^ (2 * h) * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 (zoomPointRec lam h rc zc p)

∂_R W_n in terms of the radial partial derivative of u_z.

theorem CIV.dz_zoomWRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dz (zoomWRec lam h rc zc u) p = lam * lam ^ (1 - 2 * h) * lam ^ (2 * h) * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 (zoomPointRec lam h rc zc p)

∂_Z W_n in terms of the vertical partial derivative of u_z.

theorem CIV.dr_zoomSRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dr (zoomSRec lam h rc zc u) p = lam ^ 2 * lam ^ (2 * h) * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 0 (zoomPointRec lam h rc zc p)

∂_R S_n in terms of the radial partial derivative of u_θ.

theorem CIV.dz_zoomSRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dz (zoomSRec lam h rc zc u) p = lam * lam ^ (1 - 2 * h) * lam ^ (2 * h) * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 2 (zoomPointRec lam h rc zc p)

∂_Z S_n in terms of the vertical partial derivative of u_θ.

Open-neighbourhood lemmas for the recentred zoom

theorem CIV.isOpen_zoomPointRec_preimage (lam h rc zc : ℝ) : IsOpen {q : (ℝ × ℝ) × ℝ | zoomPointRec lam h rc zc q ∈ unitCylinder}

theorem CIV.isOpen_slice_r_rec (lam h rc zc : ℝ) (p : (ℝ × ℝ) × ℝ) : IsOpen {r : ℝ | zoomPointRec lam h rc zc ((r, p.1.2), p.2) ∈ unitCylinder}

theorem CIV.isOpen_slice_z_rec (lam h rc zc : ℝ) (p : (ℝ × ℝ) × ℝ) : IsOpen {s : ℝ | zoomPointRec lam h rc zc ((p.1.1, s), p.2) ∈ unitCylinder}

theorem CIV.eventuallyEq_slice_r_rec (lam h rc zc : ℝ) (φ : (ℝ × ℝ) × ℝ → ℝ) (ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (K : ℝ) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) (hφ : ∀ (q : (ℝ × ℝ) × ℝ), zoomPointRec lam h rc zc q ∈ unitCylinder → φ q = K * ψ (zoomPointRec lam h rc zc q)) : (fun (r : ℝ) => φ ((r, p.1.2), p.2)) =ᶠ[nhds p.1.1] fun (r : ℝ) => K * ψ (zoomPointRec lam h rc zc ((r, p.1.2), p.2))

A first-order identity valid at every recentred zoom point of the unit cylinder holds on a whole neighbourhood of p.1.1 inside the radial slice through p.

theorem CIV.eventuallyEq_slice_z_rec (lam h rc zc : ℝ) (φ : (ℝ × ℝ) × ℝ → ℝ) (ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (K : ℝ) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) (hφ : ∀ (q : (ℝ × ℝ) × ℝ), zoomPointRec lam h rc zc q ∈ unitCylinder → φ q = K * ψ (zoomPointRec lam h rc zc q)) : (fun (s : ℝ) => φ ((p.1.1, s), p.2)) =ᶠ[nhds p.1.2] fun (s : ℝ) => K * ψ (zoomPointRec lam h rc zc ((p.1.1, s), p.2))

The vertical counterpart of eventuallyEq_slice_r_rec.

Second-derivative helpers for the recentred zoom

theorem CIV.hasDerivAt_spatialPartial_zero_zoomRec_r (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (i : Fin 3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : HasDerivAt (fun (r : ℝ) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 0 (zoomPointRec lam h rc zc ((r, p.1.2), p.2))) (lam * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 0 (zoomPointRec lam h rc zc p)) p.1.1

The R-derivative of spatialPartial (u· i) 0 composed with zoomPointRec.

theorem CIV.hasDerivAt_spatialPartial_two_zoomRec_r (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (i : Fin 3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : HasDerivAt (fun (r : ℝ) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 (zoomPointRec lam h rc zc ((r, p.1.2), p.2))) (lam * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 1 1 (zoomPointRec lam h rc zc p)) p.1.1

The R-derivative of spatialPartial (u· i) 2 composed with zoomPointRec.

theorem CIV.hasDerivAt_spatialPartial_two_zoomRec_z (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (i : Fin 3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : HasDerivAt (fun (s : ℝ) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 (zoomPointRec lam h rc zc ((p.1.1, s), p.2))) (lam ^ (1 - 2 * h) * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 0 2 (zoomPointRec lam h rc zc p)) p.1.2

The Z-derivative of spatialPartial (u· i) 2 composed with zoomPointRec.

Second-order chain rules for the recentred fields

theorem CIV.drdr_zoomVRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dr (dr (zoomVRec lam h rc zc u)) p = lam ^ 3 * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 0 (zoomPointRec lam h rc zc p)

theorem CIV.drdz_zoomVRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dr (dz (zoomVRec lam h rc zc u)) p = lam ^ 2 * lam ^ (1 - 2 * h) * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 1 1 (zoomPointRec lam h rc zc p)

theorem CIV.dzdz_zoomVRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dz (dz (zoomVRec lam h rc zc u)) p = lam * (lam ^ (1 - 2 * h)) ^ 2 * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 2 (zoomPointRec lam h rc zc p)

theorem CIV.drdr_zoomWRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dr (dr (zoomWRec lam h rc zc u)) p = lam ^ 3 * lam ^ (2 * h) * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 0 (zoomPointRec lam h rc zc p)

theorem CIV.drdz_zoomWRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dr (dz (zoomWRec lam h rc zc u)) p = lam ^ 2 * lam ^ (2 * h) * lam ^ (1 - 2 * h) * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 1 1 (zoomPointRec lam h rc zc p)

theorem CIV.dzdz_zoomWRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dz (dz (zoomWRec lam h rc zc u)) p = lam * lam ^ (2 * h) * (lam ^ (1 - 2 * h)) ^ 2 * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 2 (zoomPointRec lam h rc zc p)

theorem CIV.drdr_zoomSRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dr (dr (zoomSRec lam h rc zc u)) p = lam ^ 3 * lam ^ (2 * h) * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 2 0 (zoomPointRec lam h rc zc p)

theorem CIV.drdz_zoomSRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dr (dz (zoomSRec lam h rc zc u)) p = lam ^ 2 * lam ^ (2 * h) * lam ^ (1 - 2 * h) * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 1 1 (zoomPointRec lam h rc zc p)

theorem CIV.dzdz_zoomSRec (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dz (dz (zoomSRec lam h rc zc u)) p = lam * lam ^ (2 * h) * (lam ^ (1 - 2 * h)) ^ 2 * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 0 2 (zoomPointRec lam h rc zc p)

The rescaled azimuthal vorticity

theorem CIV.zoomTheta_eq (lam h rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : zoomTheta lam h rc zc u p = (lam ^ (2 * h)) ^ 2 * dz (zoomVRec lam h rc zc u) p - dr (zoomWRec lam h rc zc u) p

eq:aniso:zoom:receding:vorticity: the rescaled azimuthal vorticity is Θ_n = δ_n² ∂_Z V_n - ∂_R W_n, with δ_n = lam ^ (2 * h).

The recentred divergence identity

theorem CIV.zoomVRec_div_eq (lam h rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) (hR : p.1.1 ≠ -(rc / lam)) : zoomVRec lam h rc zc u p / (rc / lam + p.1.1) = lam ^ 2 * (u (zoomPointRec lam h rc zc p) 0 / (zoomPointRec lam h rc zc p).1 0)

Off the receding axis, the recentred radial velocity divided by A + R equals lam² times the meridional radial quotient at the recentred zoom point, with A = rc / lam.

theorem CIV.zoomRec_divergence_identity (lam h rc 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) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) (hR : p.1.1 ≠ -(rc / lam)) : dr (zoomVRec lam h rc zc u) p + zoomVRec lam h rc zc u p / (rc / lam + p.1.1) + dz (zoomWRec lam h rc zc u) p = 0

eq:aniso:zoom:receding:div: in the recentred variables the divergence-free condition reads ∂_R V_n + V_n / (A + R) + ∂_Z W_n = 0, with A = rc / lam, at every point with R ≠ -A.

The anisotropic bounds in the recentred variables (eq:aniso:zoom:derivatives)

theorem CIV.abs_zoomVRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |zoomVRec lam h rc zc u p| ≤ C * (-p.2) ^ (-(1 / 2) - 0 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_dr_zoomVRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |dr (zoomVRec lam h rc zc u) p| ≤ C * (-p.2) ^ (-(1 / 2) - 1 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_dz_zoomVRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |dz (zoomVRec lam h rc zc u) p| ≤ C * (-p.2) ^ (-(1 / 2) - 0 / 2 - (1 / 2 - h) * 1)

theorem CIV.abs_drdr_zoomVRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |dr (dr (zoomVRec lam h rc zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - 2 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_drdz_zoomVRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |dr (dz (zoomVRec lam h rc zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - 1 / 2 - (1 / 2 - h) * 1)

theorem CIV.abs_dzdz_zoomVRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |dz (dz (zoomVRec lam h rc zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - 0 / 2 - (1 / 2 - h) * 2)

theorem CIV.abs_zoomWRec_add_abs_zoomSRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |zoomWRec lam h rc zc u p| + |zoomSRec lam h rc zc u p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 0 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_dr_zoomWRec_add_abs_dr_zoomSRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |dr (zoomWRec lam h rc zc u) p| + |dr (zoomSRec lam h rc zc u) p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 1 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_dz_zoomWRec_add_abs_dz_zoomSRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |dz (zoomWRec lam h rc zc u) p| + |dz (zoomSRec lam h rc zc u) p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 0 / 2 - (1 / 2 - h) * 1)

theorem CIV.abs_drdr_zoomWRec_add_abs_drdr_zoomSRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |dr (dr (zoomWRec lam h rc zc u)) p| + |dr (dr (zoomSRec lam h rc zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 2 / 2 - (1 / 2 - h) * 0)

theorem CIV.abs_drdz_zoomWRec_add_abs_drdz_zoomSRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |dr (dz (zoomWRec lam h rc zc u)) p| + |dr (dz (zoomSRec lam h rc zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 1 / 2 - (1 / 2 - h) * 1)

theorem CIV.abs_dzdz_zoomWRec_add_abs_dzdz_zoomSRec_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |dz (dz (zoomWRec lam h rc zc u)) p| + |dz (dz (zoomSRec lam h rc zc u)) p| ≤ C * (-p.2) ^ (-(1 / 2) - h - 0 / 2 - (1 / 2 - h) * 2)

The bound on the rescaled azimuthal vorticity

theorem CIV.abs_zoomTheta_le (C h lam rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |zoomTheta lam h rc zc u p| ≤ C * ((lam ^ (2 * h)) ^ 2 * (-p.2) ^ (-1 + h) + (-p.2) ^ (-1 - h))

eq:aniso:zoom:receding:bound: with δ_n = lam ^ (2 * h) the rescaled azimuthal vorticity obeys |Θ_n| ≤ C (δ_n² |τ| ^ (-1 + h) + |τ| ^ (-1 - h)), the two terms coming from the ∂_Z V_n and ∂_R W_n entries of eq:aniso:zoom:derivatives.