Rot Field

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

noncomputable def CIV.rotField (φ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.Vec3

The rotated field (ℛ_φ u)(x, t) = Q_φ u(Q_φ⁻¹ x, t) of eq:interior:average.

Equations

• CIV.rotField φ u z = CIV.rotZ φ (u (CIV.rotZ (-φ) z.1, z.2))