First-order chain rules for the zoomed fields

The zoom map zoomPoint of eq:aniso:zoom:finite:variables sends ((r, z), τ) to the point (meridional (lam r) (zc + lam^(1-2h) z), lam² τ). Its time slot does not depend on r or on z, so the r- and z-derivatives of a zoomed field are derivatives along a straight line inside a fixed spatial slice {t = lam² τ}. Every derivative below is therefore taken on Vec3, never on the parabolic carrier itself (design note R2: ParabolicPoint carries the parabolic metric and no linear structure of its own).

The resulting formulas are the first-order part of eq:aniso:zoom:fields: ∂_r V = lam² ∂₁u₁, ∂_z V = lam · lam^{1-2h} ∂₃u₁, and the analogous identities for W and S with the extra factor lam^{2h}.

Derivatives of the meridional line

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

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

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

Moving the vertical coordinate of a meridional point at speed a moves it along e₃.

Chain rule inside a fixed time slice

theorem CIV.hasDerivAt_comp_spatialSlice {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) {f : ℝ → CKN.Foundation.Parabolic.Vec3} {a x : ℝ} {j : Fin 3} (hf : HasDerivAt f (a • CKN.basisVec j) x) (hx : f x = z.1) (i : Fin 3) : HasDerivAt (fun (s : ℝ) => u (f s, z.2) i) (a * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j z) x

A component of a C¹ field, read along a curve f that stays in the time slice of z and passes through z with velocity a • e_j, has derivative a ∂_j u_i (z). Only the spatial slice fun y : Vec3 => u (y, z.2) is differentiated, so no linear structure on the parabolic carrier is required.

The zoom map differentiated in r and in z

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

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

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

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

First-order chain rules for the rescaled fields

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

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

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

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

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

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

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

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

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

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

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

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