Derivatives of functions lifted through (X, Z, τ) ↦ (|X|, Z, τ)

A function g of the meridional variables ((R, Z), τ) is lifted to the variables (X, Z, τ) ∈ ℝ⁴ × ℝ × ℝ of eq:aniso:zoom:lifted by composing with zoomLiftPoint. Off the axis X = 0 the lift is differentiable, and its derivatives in the coordinate directions are ∂_{X_i} (g ∘ L) = ∂_R g · X_i / R, ∂_Z (g ∘ L) = ∂_Z g, ∂_τ (g ∘ L) = ∂_τ g (fderiv_comp_zoomLiftPoint_radial, fderiv_comp_zoomLiftPoint_vertical, fderiv_comp_zoomLiftPoint_time). The derivative of G ∘ L · X_i / R in the direction X_i is ∂_R G · X_i² / R² + G · (1 / R - X_i² / R³) (fderiv_comp_zoomLiftPoint_mul_dir); summed over the four radial directions this produces the radial operator ∂_RR + 3 R⁻¹ ∂_R of eq:aniso:zoom:finite:equation and the divergence ∂_R V + 3 V / R + ∂_Z W of the drift of eq:drift:Bn:def.

Meridional slices

theorem CIV.hasDerivAt_dr_of_differentiableAt {G : (ℝ × ℝ) × ℝ → ℝ} {p : (ℝ × ℝ) × ℝ} (hG : DifferentiableAt ℝ G p) : HasDerivAt (fun (r : ℝ) => G ((r, p.1.2), p.2)) (dr G p) p.1.1

The radial slice of a differentiable function has derivative dr.

theorem CIV.hasDerivAt_dz_of_differentiableAt {G : (ℝ × ℝ) × ℝ → ℝ} {p : (ℝ × ℝ) × ℝ} (hG : DifferentiableAt ℝ G p) : HasDerivAt (fun (z : ℝ) => G ((p.1.1, z), p.2)) (dz G p) p.1.2

The vertical slice of a differentiable function has derivative dz.

theorem CIV.hasDerivAt_dtPast_of_differentiableAt {G : (ℝ × ℝ) × ℝ → ℝ} {p : (ℝ × ℝ) × ℝ} (hG : DifferentiableAt ℝ G p) : HasDerivAt (fun (t : ℝ) => G (p.1, t)) (dtPast G p) p.2

The time slice of a differentiable function has derivative dtPast.

theorem CIV.dr_eq_fderiv {G : (ℝ × ℝ) × ℝ → ℝ} {p : (ℝ × ℝ) × ℝ} (hG : DifferentiableAt ℝ G p) : dr G p = (fderiv ℝ G p) ((1, 0), 0)

dr of a differentiable function is its derivative in the direction ((1, 0), 0).

theorem CIV.dz_eq_fderiv {G : (ℝ × ℝ) × ℝ → ℝ} {p : (ℝ × ℝ) × ℝ} (hG : DifferentiableAt ℝ G p) : dz G p = (fderiv ℝ G p) ((0, 1), 0)

dz of a differentiable function is its derivative in the direction ((0, 1), 0).

theorem CIV.contDiffOn_dr {G : (ℝ × ℝ) × ℝ → ℝ} {O : Set ((ℝ × ℝ) × ℝ)} (hO : IsOpen O) (hG : ContDiffOn ℝ (↑⊤) G O) : ContDiffOn ℝ (↑⊤) (dr G) O

dr of a function smooth on an open set is smooth there.

theorem CIV.contDiffOn_dz {G : (ℝ × ℝ) × ℝ → ℝ} {O : Set ((ℝ × ℝ) × ℝ)} (hO : IsOpen O) (hG : ContDiffOn ℝ (↑⊤) G O) : ContDiffOn ℝ (↑⊤) (dz G) O

dz of a function smooth on an open set is smooth there.

theorem CIV.fderiv_apply_eq_of_hasDerivAt_line {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {z v : E} {D : ℝ} (hf : DifferentiableAt ℝ f z) (hD : HasDerivAt (fun (t : ℝ) => f (z + t • v)) D 0) : (fderiv ℝ f z) v = D

A directional derivative is the derivative along the line.

The one-variable core

theorem CIV.hasDerivAt_comp_sqrt_sq_add {G : ℝ → ℝ} {G' c a r : ℝ} (hpos : 0 < a ^ 2 + c) (hr : r = √(a ^ 2 + c)) (hG : HasDerivAt G G' r) : HasDerivAt (fun (b : ℝ) => G √(b ^ 2 + c)) (G' * (a / r)) a

The chain rule through b ↦ √(b² + c).

theorem CIV.hasDerivAt_comp_sqrt_sq_add_mul_div {G : ℝ → ℝ} {G' c a r : ℝ} (hpos : 0 < a ^ 2 + c) (hr : r = √(a ^ 2 + c)) (hG : HasDerivAt G G' r) : HasDerivAt (fun (b : ℝ) => G √(b ^ 2 + c) * (b / √(b ^ 2 + c))) (G' * (a / r) ^ 2 + G r * (1 / r - a ^ 2 / r ^ 3)) a

The derivative of b ↦ G(√(b² + c)) · b / √(b² + c).

The lift

theorem CIV.differentiableAt_zoomLiftRadius {z : CKN.Vec 5 × ℝ} (hR : 0 < zoomLiftRadius z.1) : DifferentiableAt ℝ (fun (w : CKN.Vec 5 × ℝ) => zoomLiftRadius w.1) z

The lift is differentiable off the axis.

theorem CIV.differentiableAt_zoomLiftPoint {z : CKN.Vec 5 × ℝ} (hR : 0 < zoomLiftRadius z.1) : DifferentiableAt ℝ zoomLiftPoint z

The lift is differentiable off the axis.

theorem CIV.contDiffOn_zoomLiftPoint : ContDiffOn ℝ (↑⊤) zoomLiftPoint {z : CKN.Vec 5 × ℝ | 0 < zoomLiftRadius z.1}

The lift is smooth off the axis.

theorem CIV.zoomLiftPoint_add_smul_radial {z : CKN.Vec 5 × ℝ} {i : Fin 5} (hi : i ≠ 4) {c : ℝ} (hc : ∀ (s : ℝ), zoomLiftRadius (Function.update z.1 i s) = √(s ^ 2 + c)) (t : ℝ) : zoomLiftPoint (z + t • (CKN.basisVec i, 0)) = ((√((z.1 i + t) ^ 2 + c), z.1 4), z.2)

Moving along a radial coordinate direction.

theorem CIV.zoomLiftPoint_add_smul_vertical (z : CKN.Vec 5 × ℝ) (t : ℝ) : zoomLiftPoint (z + t • (CKN.basisVec 4, 0)) = ((zoomLiftRadius z.1, z.1 4 + t), z.2)

Moving along the vertical coordinate direction.

theorem CIV.zoomLiftPoint_add_smul_time (z : CKN.Vec 5 × ℝ) (t : ℝ) : zoomLiftPoint (z + t • (0, 1)) = ((zoomLiftRadius z.1, z.1 4), z.2 + t)

Moving in time.

theorem CIV.fderiv_comp_zoomLiftPoint_radial {g : (ℝ × ℝ) × ℝ → ℝ} {z : CKN.Vec 5 × ℝ} (hR : 0 < zoomLiftRadius z.1) (hg : DifferentiableAt ℝ g (zoomLiftPoint z)) {i : Fin 5} (hi : i ≠ 4) : (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => g (zoomLiftPoint w)) z) (CKN.basisVec i, 0) = dr g (zoomLiftPoint z) * (z.1 i / zoomLiftRadius z.1)

∂_{X_i} (g ∘ L) = ∂_R g · X_i / R off the axis.

theorem CIV.fderiv_comp_zoomLiftPoint_vertical {g : (ℝ × ℝ) × ℝ → ℝ} {z : CKN.Vec 5 × ℝ} (hR : 0 < zoomLiftRadius z.1) (hg : DifferentiableAt ℝ g (zoomLiftPoint z)) : (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => g (zoomLiftPoint w)) z) (CKN.basisVec 4, 0) = dz g (zoomLiftPoint z)

∂_Z (g ∘ L) = ∂_Z g off the axis.

theorem CIV.fderiv_comp_zoomLiftPoint_time {g : (ℝ × ℝ) × ℝ → ℝ} {z : CKN.Vec 5 × ℝ} (hR : 0 < zoomLiftRadius z.1) (hg : DifferentiableAt ℝ g (zoomLiftPoint z)) : (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => g (zoomLiftPoint w)) z) (0, 1) = dtPast g (zoomLiftPoint z)

∂_τ (g ∘ L) = ∂_τ g off the axis.

theorem CIV.fderiv_comp_zoomLiftPoint_mul_dir {G : (ℝ × ℝ) × ℝ → ℝ} {z : CKN.Vec 5 × ℝ} (hR : 0 < zoomLiftRadius z.1) (hG : DifferentiableAt ℝ G (zoomLiftPoint z)) {i : Fin 5} (hi : i ≠ 4) : (fderiv ℝ (fun (w : CKN.Vec 5 × ℝ) => G (zoomLiftPoint w) * (w.1 i / zoomLiftRadius w.1)) z) (CKN.basisVec i, 0) = dr G (zoomLiftPoint z) * (z.1 i / zoomLiftRadius z.1) ^ 2 + G (zoomLiftPoint z) * (1 / zoomLiftRadius z.1 - z.1 i ^ 2 / zoomLiftRadius z.1 ^ 3)

∂_{X_i} (G ∘ L · X_i / R) = ∂_R G · X_i² / R² + G · (1 / R - X_i² / R³) off the axis.