Angular Mean Scalar

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

noncomputable def CIV.angularMeanScalar (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The angular mean of a scalar field, (2π)⁻¹ ∫₀^{2π} g(Q_φ⁻¹ x, t) dφ.

Equations

• CIV.angularMeanScalar g z = (2 * Real.pi)⁻¹ • ∫ (φ : ℝ) in 0..2 * Real.pi, g (CIV.rotZ (-φ) z.1, z.2)