Meridional embedding chain rule

The meridional embedding (r, z) ↦ (r, 0, z) of CIV.meridional threads a scalar field's r- and z-derivatives along straight lines in Vec3 into Fréchet derivatives on the full spatial domain. The first-order theorems (hasDerivAt_comp_meridional_fst, hasDerivAt_comp_meridional_snd) are the unit-speed special case of CIV.hasDerivAt_meridional_fst/hasDerivAt_meridional_snd from CIV.Zoom.ChainRule.

The second-order theorems (hasDerivAt_deriv_comp_meridional_fst, hasDerivAt_deriv_comp_meridional_snd) give the derivative of the derivative, which CIV.axisMaximumPrinciple needs for its hypotheses (lem:aniso:axis).

theorem CIV.hasDerivAt_comp_meridional_fst {g : CKN.Foundation.Parabolic.Vec3 → ℝ} {r₀ x₃ : ℝ} (hg : DifferentiableAt ℝ g (meridional r₀ x₃)) : HasDerivAt (fun (r : ℝ) => g (meridional r x₃)) ((fderiv ℝ g (meridional r₀ x₃)) (CKN.basisVec 0)) r₀

First-order chain rule for a scalar composed with the r-directed meridional embedding. The embedding's derivative is the public CIV.hasDerivAt_meridional_fst of CIV.Zoom.ChainRule at unit radial speed.

theorem CIV.hasDerivAt_comp_meridional_snd {g : CKN.Foundation.Parabolic.Vec3 → ℝ} {x₁ z₀ : ℝ} (hg : DifferentiableAt ℝ g (meridional x₁ z₀)) : HasDerivAt (fun (z : ℝ) => g (meridional x₁ z)) ((fderiv ℝ g (meridional x₁ z₀)) (CKN.basisVec 2)) z₀

First-order chain rule for a scalar composed with the z-directed meridional embedding. The embedding's derivative is the public CIV.hasDerivAt_meridional_snd of CIV.Zoom.ChainRule at unit vertical speed and zero offset.

theorem CIV.isOpen_meridional_fst_preimage (x₃ : ℝ) : IsOpen {r : ℝ | meridional r x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 1}

The preimage of the unit ball under the r-directed meridional embedding is open.

theorem CIV.isOpen_meridional_snd_preimage (x₁ : ℝ) : IsOpen {z : ℝ | meridional x₁ z ∈ CKN.Foundation.Parabolic.vec3Ball 0 1}

The preimage of the unit ball under the z-directed meridional embedding is open.

theorem CIV.hasDerivAt_deriv_comp_meridional_fst {g : CKN.Foundation.Parabolic.Vec3 → ℝ} {r₀ x₃ : ℝ} (hg : ContDiffOn ℝ 2 g (CKN.Foundation.Parabolic.vec3Ball 0 1)) (hmem : meridional r₀ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 1) : HasDerivAt (fun (r : ℝ) => deriv (fun (r' : ℝ) => g (meridional r' x₃)) r) ((fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ g y) (CKN.basisVec 0)) (meridional r₀ x₃)) (CKN.basisVec 0)) r₀

Second-order chain rule for a scalar composed with the r-directed meridional embedding: the second derivative of r ↦ g (meridional r x₃) at r₀ is the corresponding iterated Fréchet derivative of g.

theorem CIV.hasDerivAt_deriv_comp_meridional_snd {g : CKN.Foundation.Parabolic.Vec3 → ℝ} {x₁ z₀ : ℝ} (hg : ContDiffOn ℝ 2 g (CKN.Foundation.Parabolic.vec3Ball 0 1)) (hmem : meridional x₁ z₀ ∈ CKN.Foundation.Parabolic.vec3Ball 0 1) : HasDerivAt (fun (z : ℝ) => deriv (fun (z' : ℝ) => g (meridional x₁ z')) z) ((fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ g y) (CKN.basisVec 2)) (meridional x₁ z₀)) (CKN.basisVec 2)) z₀

Second-order chain rule for a scalar composed with the z-directed meridional embedding.