The Laplacian of an axisymmetric field in cylindrical form

Differentiating the infinitesimal identities of CIV.Identities.Axisymmetric once more in the second Cartesian direction gives the missing second derivative on the meridional plane: for an axisymmetric scalar, ∂₂∂₂ g = r⁻¹ ∂_r g, so the Cartesian Laplacian becomes the cylindrical one ∂_r² + r⁻¹ ∂_r + ∂_z² of eq:aniso:scalar:nse:z. For the radial and swirl components of an axisymmetric field the same computation carries the source term of the infinitesimal identity and produces the extra -r⁻² of eq:aniso:scalar:nse:r and eq:aniso:scalar:nse:swirl.

The differentiation is carried out on the slice y ↦ g (y, t) of the unit ball, where the identity of angularGenerator_of_invariant holds at every point; the product rule in the direction of the second basis vector and the vanishing of the second coordinate on the meridional plane leave exactly one term.

theorem CIV.differentiableAt_spatialPartial_slice {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (i : Fin 3) : DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.spatialPartial g i (y, z.2)) z.1

A classical spatial partial derivative of a C² scalar is differentiable in space.

theorem CIV.spatialSecondPartial_one_one_of_angularGenerator {g s : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hs : DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => s (y, z.2)) z.1) (hrel : ∀ y ∈ CKN.Foundation.Parabolic.vec3Ball 0 1, -y 1 * CKN.spatialPartial g 0 (y, z.2) + y 0 * CKN.spatialPartial g 1 (y, z.2) = s (y, z.2)) (hplane : z.1 1 = 0) : z.1 0 * CKN.spatialSecondPartial g 1 1 z = CKN.spatialPartial g 0 z + CKN.spatialPartial s 1 z

Differentiating the infinitesimal identity -x₂ ∂₁g + x₁ ∂₂g = s in the second Cartesian direction: on the meridional plane the second derivative ∂₂∂₂g is determined by ∂₁g and by the second derivative of the source.

theorem CIV.spatialPartial_neg (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (i : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => -g w) i z = -CKN.spatialPartial g i z

A classical spatial partial derivative is odd under negation of the scalar.

theorem CIV.spatialPartial_zero_fun (i : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) i z = 0

The classical spatial partial derivatives of the zero scalar vanish.

The cylindrical Laplacian of an axisymmetric scalar

theorem CIV.spatialSecondPartial_one_one_of_invariant {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) (hinv : ∀ (φ : ℝ), ∀ w ∈ unitCylinder, g (rotZ φ w.1, w.2) = g w) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : CKN.spatialSecondPartial g 1 1 z = CKN.spatialPartial g 0 z / z.1 0

For a rotation-invariant C² scalar, on the meridional plane off the axis, ∂₂∂₂g = r⁻¹ ∂_r g.

theorem CIV.sum_spatialSecondPartial_of_invariant {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hg : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) (hinv : ∀ (φ : ℝ), ∀ w ∈ unitCylinder, g (rotZ φ w.1, w.2) = g w) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : ∑ j : Fin 3, CKN.spatialSecondPartial g j j z = CKN.spatialSecondPartial g 0 0 z + CKN.spatialPartial g 0 z / z.1 0 + CKN.spatialSecondPartial g 2 2 z

For a rotation-invariant C² scalar, on the meridional plane off the axis, the Cartesian Laplacian is the cylindrical Laplacian ∂_r² + r⁻¹ ∂_r + ∂_z² of eq:aniso:scalar:nse:z.

The cylindrical Laplacian of the components of an axisymmetric field

theorem CIV.spatialSecondPartial_one_one_zero_meridional {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 1 1 z = CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 z / z.1 0 - u z 0 / z.1 0 ^ 2

On the meridional plane, off the axis, the second Cartesian derivative of the radial component in the second direction is r⁻¹ ∂_r u_r - r⁻² u_r.

theorem CIV.spatialSecondPartial_one_one_one_meridional {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 1 1 z = CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 0 z / z.1 0 - u z 1 / z.1 0 ^ 2

On the meridional plane, off the axis, the second Cartesian derivative of the swirl in the second direction is r⁻¹ ∂_r u_θ - r⁻² u_θ.

theorem CIV.spatialSecondPartial_one_one_two_meridional {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 1 1 z = CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 z / z.1 0

On the meridional plane, off the axis, the second Cartesian derivative of the vertical component in the second direction is r⁻¹ ∂_r u_z.

theorem CIV.sum_spatialSecondPartial_zero_meridional {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : ∑ j : Fin 3, CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) j j z = CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 0 z + CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 z / z.1 0 + CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 2 z - u z 0 / z.1 0 ^ 2

The Cartesian Laplacian of the radial component on the meridional plane, off the axis: the cylindrical operator ∂_r² + r⁻¹ ∂_r + ∂_z² - r⁻² of eq:aniso:scalar:nse:r.

theorem CIV.sum_spatialSecondPartial_one_meridional {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : ∑ j : Fin 3, CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) j j z = CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 0 0 z + CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 0 z / z.1 0 + CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 2 2 z - u z 1 / z.1 0 ^ 2

The Cartesian Laplacian of the swirl on the meridional plane, off the axis: the cylindrical operator ∂_r² + r⁻¹ ∂_r + ∂_z² - r⁻² of eq:aniso:scalar:nse:swirl.

theorem CIV.sum_spatialSecondPartial_two_meridional {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : ∑ j : Fin 3, CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) j j z = CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 0 z + CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 z / z.1 0 + CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 2 z

The Cartesian Laplacian of the vertical component on the meridional plane, off the axis: the cylindrical operator ∂_r² + r⁻¹ ∂_r + ∂_z² of eq:aniso:scalar:nse:z.