Angular Mean

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

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

The angular mean 𝒫u = (2π)⁻¹ ∫₀^{2π} ℛ_φ u dφ of eq:interior:average, the axisymmetric part of a field.

Equations

• CIV.angularMean u z = (2 * Real.pi)⁻¹ • ∫ (φ : ℝ) in 0..2 * Real.pi, CIV.rotField φ u z