Rotation covariance and the averaged classical solution (sec:reduction:core)

The forced Navier–Stokes system eq:nse:forced is covariant under the rigid rotations Q_φ of CIV.rotZ: if (u, p, f) is a classical solution on the unit cylinder then so is the rotated triple (ℛ_φ u, p ∘ Q_φ⁻¹, ℛ_φ f) (isClassicalSolutionOn_rotField). Design note R8 records the reduction this feeds: since an axisymmetric u is fixed by every ℛ_φ, averaging the rotated triples in φ over [0, 2π] replaces (u, p, f) by (u, 𝒫p, 𝒫f), again a classical solution (isClassicalSolutionOn_angularMean), with an axisymmetric, C²-bounded force when the original force was C²-bounded (forceC2Bounded_angularMean).

The derivative of the rotated field

theorem CIV.fderiv_rotField_spatial (φ : ℝ) (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) (w : CKN.Foundation.Parabolic.Vec3) : (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => rotField φ u (y, z.2)) z.1) w = rotZ φ ((fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, z.2)) (rotZ (-φ) z.1)) (rotZ (-φ) w))

The derivative of rotField with respect to the space variable.

theorem CIV.contDiffOn_rotField (φ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => rotField φ u z) unitCylinder

rotField at a fixed angle is C¹ on the unit cylinder whenever u is.

theorem CIV.spatialPartial_comp_rotZ (ψ : ℝ) (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g (rotZ ψ w.1, w.2)) i z = (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => g (y, z.2)) (rotZ ψ z.1)) (rotZ ψ (CKN.basisVec i))

The spatial partial derivative of a scalar field composed with a rotation of the point is the corresponding partial derivative of the field at the rotated point, in the rotated direction. Unconditional: no regularity hypothesis on g is needed.

The time derivative of the rotated field

theorem CIV.timePartial_rotField_zero (φ : ℝ) (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) : CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => rotField φ u w 0) z = Real.cos φ * CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) (rotZ (-φ) z.1, z.2) - Real.sin φ * CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) (rotZ (-φ) z.1, z.2)

The time derivative of rotField, component 0.

theorem CIV.timePartial_rotField_one (φ : ℝ) (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) : CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => rotField φ u w 1) z = Real.sin φ * CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) (rotZ (-φ) z.1, z.2) + Real.cos φ * CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) (rotZ (-φ) z.1, z.2)

The time derivative of rotField, component 1.

theorem CIV.timePartial_rotField_two (φ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => rotField φ u w 2) z = CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) (rotZ (-φ) z.1, z.2)

The time derivative of rotField, component 2.

The spatial derivatives of the rotated field

theorem CIV.spatialPartial_rotField_zero (φ : ℝ) (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) (j : Fin 3) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => rotField φ u w 0) j z = Real.cos φ * (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, z.2) 0) (rotZ (-φ) z.1)) (rotZ (-φ) (CKN.basisVec j)) - Real.sin φ * (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, z.2) 1) (rotZ (-φ) z.1)) (rotZ (-φ) (CKN.basisVec j))

A spatial partial derivative of rotField, component 0.

theorem CIV.spatialPartial_rotField_one (φ : ℝ) (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) (j : Fin 3) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => rotField φ u w 1) j z = Real.sin φ * (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, z.2) 0) (rotZ (-φ) z.1)) (rotZ (-φ) (CKN.basisVec j)) + Real.cos φ * (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, z.2) 1) (rotZ (-φ) z.1)) (rotZ (-φ) (CKN.basisVec j))

A spatial partial derivative of rotField, component 1.

theorem CIV.spatialPartial_rotField_two (φ : ℝ) (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) (j : Fin 3) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => rotField φ u w 2) j z = (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, z.2) 2) (rotZ (-φ) z.1)) (rotZ (-φ) (CKN.basisVec j))

A spatial partial derivative of rotField, component 2.

The Laplacian of a rotated scalar field

theorem CIV.differentiableAt_fderiv_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) (w : CKN.Foundation.Parabolic.Vec3) : DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => g (y', z.2)) y) w) z.1

Differentiability, at a general fixed direction w (not necessarily a basis vector), of the once-differentiated slice of a C² field.

noncomputable def CIV.hessAt (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (t : ℝ) (x v w : CKN.Foundation.Parabolic.Vec3) : ℝ

The second directional derivative of a C² scalar field, in directions v (outer) and w (inner). Diagonal values at basis vectors recover spatialSecondPartial (hessAt_eq_spatialSecondPartial).

Equations

• CIV.hessAt g t x v w = (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (y' : CKN.Foundation.Parabolic.Vec3) => g (y', t)) y) w) x) v

theorem CIV.hessAt_add_left (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (t : ℝ) (x v1 v2 w : CKN.Foundation.Parabolic.Vec3) : hessAt g t x (v1 + v2) w = hessAt g t x v1 w + hessAt g t x v2 w

theorem CIV.hessAt_smul_left (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (t : ℝ) (x : CKN.Foundation.Parabolic.Vec3) (c : ℝ) (v w : CKN.Foundation.Parabolic.Vec3) : hessAt g t x (c • v) w = c * hessAt g t x v w

theorem CIV.hessAt_add_right {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) (v w1 w2 : CKN.Foundation.Parabolic.Vec3) : hessAt g z.2 z.1 v (w1 + w2) = hessAt g z.2 z.1 v w1 + hessAt g z.2 z.1 v w2

theorem CIV.hessAt_const_mul_right {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) (v : CKN.Foundation.Parabolic.Vec3) (c : ℝ) (w : CKN.Foundation.Parabolic.Vec3) : hessAt g z.2 z.1 v (c • w) = c * hessAt g z.2 z.1 v w

theorem CIV.hessAt_comp_rotZ (ψ : ℝ) (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (v w : CKN.Foundation.Parabolic.Vec3) : hessAt (fun (w' : CKN.Foundation.Parabolic.ParabolicPoint) => g (rotZ ψ w'.1, w'.2)) z.2 z.1 v w = hessAt g z.2 (rotZ ψ z.1) (rotZ ψ v) (rotZ ψ w)

theorem CIV.sum_spatialSecondPartial_comp_rotZ {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) : ∑ j : Fin 3, CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g (rotZ ψ w.1, w.2)) j j z = ∑ a : Fin 3, CKN.spatialSecondPartial g a a (rotZ ψ z.1, z.2)

The Laplacian (sum of second Cartesian partial derivatives) of a C² scalar field composed with a rotation of the point is the Laplacian of the field at the rotated point: the trace of the Hessian is invariant under the orthogonal map rotZ.

theorem CIV.contDiffOn_component_comp_rotZ (ψ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (k : Fin 3) : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u (rotZ ψ z.1, z.2) k) unitCylinder

ContDiffOn of a component of u composed with a rotation of the point.

The convective and divergence terms of the rotated system

Rotation covariance of the Navier–Stokes equations

theorem CIV.isClassicalSolutionOn_rotField (φ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u p f unitCylinder) : IsClassicalSolutionOn (rotField φ u) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => p (rotZ (-φ) z.1, z.2)) (rotField φ f) unitCylinder

The Navier–Stokes equations are covariant under rigid rotations of the spatial coordinates (sec:reduction:core, design note R8). For any angle φ, if (u, p, f) solves the forced Navier–Stokes equations on the unit cylinder, then the rotated triple (ℛ_φ u, p ∘ Q_φ⁻¹, ℛ_φ f) also solves them.

The averaged classical solution

theorem CIV.contDiffOn_angularMeanScalar (n : ℕ∞) {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hp : ContDiffOn ℝ (↑n) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) : ContDiffOn ℝ (↑n) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => angularMeanScalar p z) unitCylinder

The angular mean of a C^n scalar field on the unit cylinder is C^n there.

theorem CIV.spatialPartial_angularMeanScalar {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hp : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (j : Fin 3) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => angularMeanScalar p w) j z = (2 * Real.pi)⁻¹ * ∫ (φ : ℝ) in 0..2 * Real.pi, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => p (rotZ (-φ) w.1, w.2)) j z

For a C¹ scalar field, a spatial partial derivative of the angular mean is the angular mean of the corresponding spatial partial derivatives of the rotated fields: the derivative passes under the angular integral.

theorem CIV.angularMean_apply_eq (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (i : Fin 3) : angularMean f z i = (2 * Real.pi)⁻¹ * ∫ (φ : ℝ) in 0..2 * Real.pi, rotField φ f z i

A component of the angular mean of a C^∞ vector field is the angular mean of the corresponding component of the rotated fields.

theorem CIV.spatialPartial_congr_of_eqOn {v u : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (h : ∀ w ∈ unitCylinder, v w = u w) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (j : Fin 3) : CKN.spatialPartial v j z = CKN.spatialPartial u j z

Pointwise agreement of two scalar fields on the unit cylinder transports a spatial partial derivative.

theorem CIV.isClassicalSolutionOn_angularMean (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u p f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) : IsClassicalSolutionOn u (angularMeanScalar p) (angularMean f) unitCylinder

The angular mean of a classical solution with axisymmetric velocity is again a classical solution, with pressure and force replaced by their angular means (sec:reduction:core, design note R8). Since the velocity is fixed by every rotation, only the pressure and force terms of the momentum equation change under averaging; the momentum and divergence equations themselves are linear in (p, f) with u fixed, so they survive averaging over φ.

Corollaries

theorem CIV.isAxisymmetricOn_angularMean_force (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : IsAxisymmetricOn (angularMean f) unitCylinder

The angular mean of a vector field is axisymmetric.