From the meridional plane to the whole ball #
The identities gradient_sq_meridional and stretching_meridional are proved on the
meridional plane {x₂ = 0}, off the axis. This file supplies the transfer that extends
them to every point of B(1): polar coordinates in the first two components write any
point as rotZ φ (meridional x₁ x₃) with x₁ ≥ 0 (exists_rotZ_meridional), and a
rotation-invariant quantity therefore agrees with its meridional-plane value at every
point (invariant_eq_meridional).
The Cartesian expressions spatialPartial (fun w => u w i) j are not themselves
rotation invariant: differentiating in a fixed Cartesian direction at a rotated point is
not the same operation as differentiating at the reference point. What is rotation
invariant is the pair of facts recorded here. First, the cylindrical coefficients of an
axisymmetric field, read by undoing the rotation of the field values
(cylindricalCoeffs_eq_meridional and its three components), reduce to the values on the
meridional plane; this is design note R7's identification, made precise. Second, the
scalars that actually appear in eq:aniso:closure:gradient and
eq:aniso:closure:stretch — the Frobenius norm of the full spatial derivative, the
Euclidean norm of the curl, and the vortex-stretching scalar (ω · ∇u) · ω — are
genuinely invariant under every rotation about the axis (gradient_sq_rotZ_invariant,
curl_sq_rotZ_invariant, stretching_rotZ_invariant), because fderiv_comp_rotZ
intertwines the spatial derivative with the rotations and rotZ is an orthogonal map.
Three consequences are recorded here as well. The curl itself is equivariant
(curlVec_rotZ_eq), hence so is the azimuthal vorticity, and the vorticity read as a
vector field (vorticityField) is axisymmetric (isAxisymmetricOn_vorticityField). The
circulation Γ = r u_θ is invariant (circulation_rotZ_invariant), which makes swirlCoeffAt u z = Γ / r a public
reading of u_θ at a general point, equal on the polar representative to the meridional
value (swirlCoeffAt_rotZ_meridional). Finally gradient_sq_ball and stretching_ball
glue gradient_sq_meridional and stretching_meridional to every off-axis point of B(1).
The polar representative #
Every point of Vec3 is the image, under some rotation about the vertical axis, of a
meridional point (x₁, 0, x₃) with x₁ ≥ 0 and the same third coordinate: polar
coordinates in the first two components, taking x₁ to be the modulus and φ the
argument of the complex number formed from them.
The Euclidean norm of a rotated meridional point is the norm of its meridional
coordinates: ‖rotZ φ (x₁, 0, x₃)‖ = √(x₁² + x₃²).
The general invariance transfer #
A scalar fixed by every rotation about the axis, at every point of the unit
cylinder, agrees at each point with its value at some x₁ ≥ 0 representative of the
meridional plane: the transfer that extends a meridional-plane identity to all of
B(1) (design note R7).
The cylindrical coefficients are read on the meridional plane #
At the representative point x = rotZ φ (meridional x₁ x₃), undoing the rotation of
the field value recovers the value on the meridional plane: the cylindrical coefficients
u_r (x, t) := (rotZ (-φ) (u (x, t))) 0, u_θ (x, t) := (rotZ (-φ) (u (x, t))) 1, and
u_z (x, t) := u (x, t) 2 all equal the corresponding component of u (meridional x₁ x₃, t) (design note R7).
The radial coefficient u_r at the representative point is u (meridional x₁ x₃, t) 0.
The swirl coefficient u_θ at the representative point is u (meridional x₁ x₃, t) 1.
The vertical coefficient u_z at the representative point is u (meridional x₁ x₃, t) 2; unlike the radial and swirl coefficients it needs no undoing of the rotation,
since rotZ fixes the vertical component.
The circulation and the swirl coefficient at a general point #
The circulation Γ = r u_θ = x₁u₂ − x₂u₁ of an axisymmetric field is invariant under the
rotations about the axis: the position and the field value rotate together, and the two
cos/sin pairs cancel against each other.
The swirl coefficient u_θ read at a general point: the circulation Γ = r u_θ
divided by the distance r = √(x₁² + x₂²) to the axis. This is the public reading of the
azimuthal component of the field in the cylindrical frame. On the axis the quotient is
0 / 0, whose value in Lean is 0; for an axisymmetric field that value is the correct
one, since apply_axis_one forces u_θ = 0 there, so the definition needs no caveat.
Equations
- CIV.swirlCoeffAt u z = CIV.circulation u z / √(z.1 0 ^ 2 + z.1 1 ^ 2)
Instances For
At the polar representative x = rotZ φ (meridional x₁ x₃) with x₁ > 0, the swirl
coefficient of an axisymmetric field is the second component of its value on the meridional
plane. Together with exists_rotZ_meridional this carries a meridional-plane bound on u_θ,
such as the conclusion of CIV.swirl_bound, to every point of the ball off the axis.
Rotation invariance of the basis vectors under rotZ #
The spatial derivative at a rotated point, evaluated at a fixed basis vector #
The gradient-squared is rotation invariant #
The full Cartesian gradient-squared ∑ᵢ ∑ⱼ (∂ⱼ uᵢ)² of a smooth axisymmetric field —
the Frobenius norm of the spatial derivative — is invariant under the rotations about the
axis. This is the genuinely rotation-invariant scalar behind gradient_sq_meridional
(eq:aniso:closure:gradient): the Cartesian partial derivatives themselves are not
invariant, but fderiv_comp_rotZ intertwines the full derivative with rotZ, and the
Frobenius norm is unchanged by conjugation with an orthogonal map.
The curl-squared is rotation invariant #
The curl vector fun i => curlComp u i at the rotated point is the rotation of the
curl vector at the reference point: the curl of an axisymmetric field is equivariant
under the rotations about the axis.
The vorticity as a vector field #
The Cartesian vorticity ω = ∇ × u, read as a space-time vector field.
Equations
- CIV.vorticityField u z i = CIV.curlComp u i z
Instances For
The vorticity field of a smooth axisymmetric velocity is fixed by every rotation about
the axis: the curl is equivariant (curlVec_rotZ_eq), so rotating the field value undoes
the rotation of the point.
The vorticity of a smooth axisymmetric velocity is itself axisymmetric on the unit
cylinder. This is the hypothesis gradient_sq_ball needs before it can be applied to
ω = ∇ × u.
The Cartesian curl-squared ∑ᵢ (curlComp u i)² of a smooth axisymmetric field — the
Euclidean norm of the curl — is invariant under the rotations about the axis: the curl is
equivariant (curlVec_rotZ_eq) and rotZ preserves the Euclidean norm.
The vortex-stretching scalar is rotation invariant #
The vortex-stretching scalar (ω · ∇u) · ω of eq:aniso:closure:stretch is invariant
under the rotations about the axis. Reassembled as the dot product ω · Du(ω)
(stretching_eq_dot), invariance follows from the equivariance of the curl
(curlVec_rotZ_eq), the intertwining fderiv_comp_rotZ, and the orthogonal invariance
of the dot product (rotZ_dot_rotZ).
The two meridional identities on the whole ball #
The gluing of gradient_sq_meridional to a general off-axis point of the unit cylinder:
the Frobenius norm of ∇u there equals the meridional expression at the polar representative
(x₁, 0, x₃), whose radial coordinate is positive because the point is off the axis.
The gluing of stretching_meridional to a general off-axis point of the unit cylinder:
the vortex-stretching scalar (ω · ∇u) · ω there equals its value at the polar
representative (x₁, 0, x₃), with x₁ > 0.