Documentation

LeanPool.CIVAxisymmetric.Zoom.ChainRuleSecond

Second-order zoom chain rules #

For (a,b) ∈ {(2,0),(1,1),(0,2)} and each of the three rescaled fields zoomV, zoomW, zoomS, nine theorems giving (dr)^[a] ((dz)^[b] F) p in terms of meridionalPartial.

The first-order identities (1,0) and (0,1) are already in CIV.Zoom.ChainRule.

Open-neighbourhood lemmas #

source
theorem CIV.isOpen_zoomPoint_preimage (lam h zc : ℝ) :
IsOpen {q : (ℝ × ℝ) × ℝ | zoomPoint lam h zc q ∈ unitCylinder}
source
theorem CIV.isOpen_slice_r (lam h zc : ℝ) (p : (ℝ × ℝ) × ℝ) :
IsOpen {r : ℝ | zoomPoint lam h zc ((r, p.1.2), p.2) ∈ unitCylinder}
source
theorem CIV.isOpen_slice_z (lam h zc : ℝ) (p : (ℝ × ℝ) × ℝ) :
IsOpen {s : ℝ | zoomPoint lam h zc ((p.1.1, s), p.2) ∈ unitCylinder}

First-order identities on slices #

source
theorem CIV.eventually_dr_on_slice_r (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) :
(fun (r : ℝ) => dr (zoomV lam h zc u) ((r, p.1.2), p.2)) =ᶠ[nhds p.1.1] fun (r : ℝ) => lam ^ 2 * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (zoomPoint lam h zc ((r, p.1.2), p.2))
source
theorem CIV.eventually_dz_on_slice_r (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) :
(fun (r : ℝ) => dz (zoomV lam h zc u) ((r, p.1.2), p.2)) =ᶠ[nhds p.1.1] fun (r : ℝ) => lam * lam ^ (1 - 2 * h) * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 (zoomPoint lam h zc ((r, p.1.2), p.2))
source
theorem CIV.eventually_dr_on_slice_z (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) :
(fun (s : ℝ) => dr (zoomV lam h zc u) ((p.1.1, s), p.2)) =ᶠ[nhds p.1.2] fun (s : ℝ) => lam ^ 2 * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (zoomPoint lam h zc ((p.1.1, s), p.2))
source
theorem CIV.eventually_dz_on_slice_z (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPoint lam h zc p ∈ unitCylinder) :
(fun (s : ℝ) => dz (zoomV lam h zc u) ((p.1.1, s), p.2)) =ᶠ[nhds p.1.2] fun (s : ℝ) => lam * lam ^ (1 - 2 * h) * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 (zoomPoint lam h zc ((p.1.1, s), p.2))

ContDiffOn bridges for iterated spatialPartial vector fields #

source
theorem CIV.contDiffOn_spatialPartial_vec0 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (i : Fin 3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) :
ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ![CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 0 z, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 0 z, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 0 z]) unitCylinder
source
theorem CIV.contDiffOn_spatialPartial_vec2 (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (i : Fin 3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) :
ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ![CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 z, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 z, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 z]) unitCylinder

Second-derivative helpers via hasDerivAt_comp_spatialSlice #

source
theorem CIV.hasDerivAt_spatialPartial_zero_zoom_r (lam h 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 : zoomPoint lam h zc p ∈ unitCylinder) :
HasDerivAt (fun (r : ℝ) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 0 (zoomPoint lam h zc ((r, p.1.2), p.2))) (lam * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 0 (zoomPoint lam h zc p)) p.1.1

r-derivative of spatialPartial (u· i) 0 composed with zoomPoint. Returns lam * meridionalPartial (u· i) 2 0 (zoomPoint lam h zc p).

source
theorem CIV.hasDerivAt_spatialPartial_two_zoom_r (lam h 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 : zoomPoint lam h zc p ∈ unitCylinder) :
HasDerivAt (fun (r : ℝ) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 (zoomPoint lam h zc ((r, p.1.2), p.2))) (lam * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 1 1 (zoomPoint lam h zc p)) p.1.1

r-derivative of spatialPartial (u· i) 2 composed with zoomPoint. Returns lam * meridionalPartial (u· i) 1 1 (zoomPoint lam h zc p).

source
theorem CIV.hasDerivAt_spatialPartial_two_zoom_z (lam h 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 : zoomPoint lam h zc p ∈ unitCylinder) :
HasDerivAt (fun (s : ℝ) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 (zoomPoint lam h zc ((p.1.1, s), p.2))) (lam ^ (1 - 2 * h) * meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 0 2 (zoomPoint lam h zc p)) p.1.2

z-derivative of spatialPartial (u· i) 2 composed with zoomPoint. Returns lam^(1-2h) * meridionalPartial (u· i) 0 2 (zoomPoint lam h zc p).

dr² of zoomV #

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

dr dz of zoomV #

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

dz² of zoomV #

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

dr² of zoomW #

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

dr dz of zoomW #

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

dz² of zoomW #

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

dr² of zoomS #

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

dr dz of zoomS #

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

dz² of zoomS #

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