Rotation invariance of the vertical-derivative velocity gradient

gradientSq_eq_polarR and curlSq_eq_polarR transfer the Frobenius norm of ∇u and the Euclidean norm of curl u from a general point of the unit ball to its meridional representative. The elliptic Cauchy–Schwarz step of eq:aniso:closure:mixed:bound needs the same transfer one derivative order higher, for the second-derivative factor ∂_z (∂_r u_z) = ∂_z∂_r u_z of eq:aniso:closure:mixed: this file supplies it by observing that ∂_z u is itself a smooth axisymmetric field, so gradientSq_eq_polarR applies to it directly.

The vertical derivative ∂_z u, read componentwise (dzVel), intertwines the rotations about the axis exactly as u does: fderiv_comp_rotZ applied to the direction basisVec 2, which every rotZ φ fixes, gives dzVel u (rotZ φ x, t) = rotZ φ (dzVel u (x, t)) (dzVel_rotZ_eq), hence dzVel u is axisymmetric on the unit cylinder (isAxisymmetricOn_dzVel) and, being a spatial derivative of a smooth field, is itself smooth there (contDiffOn_dzVel). Feeding these into gradientSq_eq_polarR gives the invariance of ∑ᵢⱼ (∂ⱼ∂_z uᵢ)² (dzGradientSq_eq_polarR), which is exactly the sum containing (∂_z∂_r u_z)² = (spatialSecondPartial (u_z) 0 2)² as one term.

The vertical derivative of the velocity, componentwise

noncomputable def CIV.dzVel (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.Vec3

The vertical spatial derivative of the velocity, read componentwise: ∂_z u.

Equations

• CIV.dzVel u z i = CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 z

theorem CIV.rotZ_basisVec_two (φ : ℝ) : rotZ φ (CKN.basisVec 2) = CKN.basisVec 2

Every rotation about the axis fixes the vertical basis vector.

theorem CIV.dzVel_eq_fderiv {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) : dzVel u z = (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, z.2)) z.1) (CKN.basisVec 2)

dzVel agrees with the full spatial derivative applied to the vertical basis vector.

theorem CIV.dzVel_rotZ_eq {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (φ : ℝ) : dzVel u (rotZ φ z.1, z.2) = rotZ φ (dzVel u z)

dzVel intertwines the rotations about the axis, exactly like the velocity field itself: fderiv_comp_rotZ at the direction basisVec 2, which every rotation fixes.

theorem CIV.rotField_dzVel_eq {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (φ : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) : rotField φ (dzVel u) z = dzVel u z

dzVel u is fixed by every rotation about the axis, in the rotField sense.

theorem CIV.isAxisymmetricOn_dzVel {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : IsAxisymmetricOn (dzVel u) unitCylinder

dzVel u is axisymmetric on the unit cylinder whenever u is.

theorem CIV.contDiffOn_dzVel {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => dzVel u z) unitCylinder

dzVel u is smooth on the unit cylinder whenever u is: it is a classical spatial partial derivative of each component of u.

The transfer to the meridional representative

theorem CIV.dzGradientSq_eq_polarR {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {x : CKN.Foundation.Parabolic.Vec3} {t : ℝ} (hz : (x, t) ∈ unitCylinder) : ∑ i : Fin 3, ∑ j : Fin 3, CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 j (x, t) ^ 2 = ∑ i : Fin 3, ∑ j : Fin 3, CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) 2 j (meridional (polarR x) (x 2), t) ^ 2

The rotation invariance behind eq:aniso:closure:mixed:bound's Cauchy–Schwarz step. The sum ∑ᵢⱼ (∂ⱼ∂_z uᵢ)² — the Frobenius norm of the gradient of ∂_z u — is invariant under the rotations about the axis, transferring the value at a general point to the value at its meridional representative exactly as gradientSq_eq_polarR does for ∇u itself: ∂_z u is again a smooth axisymmetric field (isAxisymmetricOn_dzVel, contDiffOn_dzVel), so gradientSq_eq_polarR applies to it directly.