Chain rules for a general scalar composed with the zoom map

CIV.Zoom.ChainRule and CIV.Zoom.ChainRuleSecond differentiate the components of a vector field along the zoom map zoomPoint of eq:aniso:zoom:finite:variables. The rescaled potential vorticity Ω_n of eq:aniso:zoom:fields is instead a plain scalar Φ : ParabolicPoint → ℝ, and — unlike the velocity — it is only smooth off the axis, so the chain rules below are stated on an arbitrary open subset D of the product carrier Vec3 × ℝ rather than on unitCylinder.

The zoom map sends ((R, Z), τ) to (meridional (lam R) (zc + lam^{1-2h} Z), lam² τ). Its time slot does not depend on R or Z and its space slot does not depend on τ, so:

• ∂_R (Φ ∘ zoomPoint) = lam ∂₁Φ,
• ∂_Z (Φ ∘ zoomPoint) = lam^{1-2h} ∂₃Φ,
• ∂_τ (Φ ∘ zoomPoint) = lam² ∂_tΦ,

with the corresponding products for the three second-order meridional derivatives. Every spatial derivative is taken on Vec3 and every time derivative on ℝ, never on the parabolic carrier itself (design note R2: ParabolicPoint carries the parabolic metric and no linear structure of its own).

The time derivative dtPast is a derivWithin over the past Iic τ; since the zoom is affine in τ the two-sided derivative exists, and HasDerivWithinAt.derivWithin together with uniqueDiffWithinAt_Iic turns it into the honest one-sided value.

Slices of a scalar field on an open set

theorem CIV.differentiableAt_spatialSlice_of_isOpen {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ D) : DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => Phi (y, z.2)) z.1

The spatial slice of a C¹ scalar is differentiable at every point of an open set.

theorem CIV.differentiableAt_timeSlice_of_isOpen {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ D) : DifferentiableAt ℝ (fun (s : ℝ) => Phi (z.1, s)) z.2

The time slice of a C¹ scalar is differentiable at every point of an open set.

theorem CIV.hasDerivAt_comp_spatialSlice_scalar {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ D) {cu : ℝ → CKN.Foundation.Parabolic.Vec3} {a x : ℝ} {j : Fin 3} (hcu : HasDerivAt cu (a • CKN.basisVec j) x) (hx : cu x = z.1) : HasDerivAt (fun (s : ℝ) => Phi (cu s, z.2)) (a * CKN.spatialPartial Phi j z) x

A C¹ scalar read along a curve cu that stays in the time slice of z and passes through z with velocity a • e_j has derivative a ∂_j Φ (z). Only the spatial slice fun y : Vec3 => Φ (y, z.2) is differentiated.

Openness of the zoom preimage and of its coordinate slices

theorem CIV.isOpen_zoomPoint_preimage_of_isOpen (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) : IsOpen {q : (ℝ × ℝ) × ℝ | zoomPoint lam h zc q ∈ D}

The preimage of an open set under the zoom map is open.

theorem CIV.isOpen_zoomSlice_r (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) (p : (ℝ × ℝ) × ℝ) : IsOpen {r : ℝ | zoomPoint lam h zc ((r, p.1.2), p.2) ∈ D}

The radial slice of the zoom preimage of an open set is open.

theorem CIV.isOpen_zoomSlice_z (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) (p : (ℝ × ℝ) × ℝ) : IsOpen {s : ℝ | zoomPoint lam h zc ((p.1.1, s), p.2) ∈ D}

The vertical slice of the zoom preimage of an open set is open.

The three one-dimensional derivatives of Φ ∘ zoomPoint

theorem CIV.hasDerivAt_zoomScalar_r (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ D) : HasDerivAt (fun (r : ℝ) => Phi (zoomPoint lam h zc ((r, p.1.2), p.2))) (lam * CKN.spatialPartial Phi 0 (zoomPoint lam h zc p)) p.1.1

Differentiating a scalar along the zoom map in the radial variable.

theorem CIV.hasDerivAt_zoomScalar_z (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ D) : HasDerivAt (fun (s : ℝ) => Phi (zoomPoint lam h zc ((p.1.1, s), p.2))) (lam ^ (1 - 2 * h) * CKN.spatialPartial Phi 2 (zoomPoint lam h zc p)) p.1.2

Differentiating a scalar along the zoom map in the vertical variable.

theorem CIV.hasDerivAt_zoomScalar_t (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ D) : HasDerivAt (fun (t : ℝ) => Phi (zoomPoint lam h zc (p.1, t))) (lam ^ 2 * CKN.timePartial Phi (zoomPoint lam h zc p)) p.2

Differentiating a scalar along the zoom map in the time variable. The zoom is affine in τ with slope lam ^ 2, so the two-sided derivative exists.

First-order chain rules

theorem CIV.dr_comp_zoomPoint (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ D) : dr (fun (q : (ℝ × ℝ) × ℝ) => Phi (zoomPoint lam h zc q)) p = lam * CKN.spatialPartial Phi 0 (zoomPoint lam h zc p)

∂_R of a scalar composed with the zoom map.

theorem CIV.dz_comp_zoomPoint (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ D) : dz (fun (q : (ℝ × ℝ) × ℝ) => Phi (zoomPoint lam h zc q)) p = lam ^ (1 - 2 * h) * CKN.spatialPartial Phi 2 (zoomPoint lam h zc p)

∂_Z of a scalar composed with the zoom map.

theorem CIV.dtPast_comp_zoomPoint (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ D) : dtPast (fun (q : (ℝ × ℝ) × ℝ) => Phi (zoomPoint lam h zc q)) p = lam ^ 2 * CKN.timePartial Phi (zoomPoint lam h zc p)

∂_τ from the past of a scalar composed with the zoom map.

Smoothness of a spatial partial derivative on an open set

theorem CIV.contDiffOn_spatialPartial_of_isOpen {n : ℕ} {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ (↑n + 1) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) (i : Fin 3) : ContDiffOn ℝ (↑n) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial Phi i z) D

A C^{n+1} scalar has C^n spatial partial derivatives on any open set.

Second-order chain rules

theorem CIV.drdr_comp_zoomPoint (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ D) : dr (dr fun (q : (ℝ × ℝ) × ℝ) => Phi (zoomPoint lam h zc q)) p = lam ^ 2 * meridionalPartial Phi 2 0 (zoomPoint lam h zc p)

∂_R∂_R of a scalar composed with the zoom map.

theorem CIV.drdz_comp_zoomPoint (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ D) : dr (dz fun (q : (ℝ × ℝ) × ℝ) => Phi (zoomPoint lam h zc q)) p = lam * lam ^ (1 - 2 * h) * meridionalPartial Phi 1 1 (zoomPoint lam h zc p)

∂_R∂_Z of a scalar composed with the zoom map.

theorem CIV.dzdz_comp_zoomPoint (lam h zc : ℝ) {D : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hD : IsOpen D) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) D) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ D) : dz (dz fun (q : (ℝ × ℝ) × ℝ) => Phi (zoomPoint lam h zc q)) p = (lam ^ (1 - 2 * h)) ^ 2 * meridionalPartial Phi 0 2 (zoomPoint lam h zc p)

∂_Z∂_Z of a scalar composed with the zoom map.