The actual L² angular average equals the literal mean of every continuous H³ representative.

theorem EulerCylinderAngleAverage.average_full_translation (P : ℝ) [Fact (0 < P)] (a : EulerLiftedGradientSpace.LiftDomain P) (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) : (average P) ((EulerLiftedGradientSpace.translation P a) u) = (EulerLiftedGradientSpace.translation P a) ((average P) u)

noncomputable def EulerCylinderAngleAverage.sobolevAverage (P : ℝ) [Fact (0 < P)] (q : ℕ) : ↥(EulerCylinderSobolevSpace.SobolevSpace P q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace P q)

Sobolev average, given by liftOperator P q (average P) (average_full_translation P).

Equations

• EulerCylinderAngleAverage.sobolevAverage P q = EulerCylinderSobolevSpace.liftOperator P q (EulerCylinderAngleAverage.average P) ⋯

theorem EulerCylinderAngleAverage.sobolevAverage_norm (P : ℝ) [Fact (0 < P)] (q : ℕ) : ‖sobolevAverage P q‖ ≤ 1

theorem EulerCylinderAngleAverage.sobolevAngleCurve_continuous (P : ℝ) [Fact (0 < P)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P q)) : Continuous fun (s : ℝ) => (EulerCylinderSobolevSpace.sobolevTranslation P q (EulerCylinderAnglePrimitive.angleShift P s)) u

theorem EulerCylinderAngleAverage.sobolevAverage_eq_integral (P : ℝ) [Fact (0 < P)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P q)) : (sobolevAverage P q) u = P⁻¹ • ∫ (s : ℝ) in 0..P, (EulerCylinderSobolevSpace.sobolevTranslation P q (EulerCylinderAnglePrimitive.angleShift P s)) u

theorem EulerCylinderAngleAverage.pointEvaluation_average_kernel (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (x : EulerLiftedGradientSpace.LiftDomain P) : (EulerSobolevPointEvaluation.pointEvaluation P x) ((sobolevAverage P 3) u) = P⁻¹ • ∫ (s : ℝ) in 0..P, EulerSobolevPointEvaluation.representative P u (x + EulerCylinderAnglePrimitive.angleShift P s)

theorem EulerCylinderAngleAverage.pointEvaluation_average_mean (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : Continuous f) (hrep : ↑↑(EulerCylinderSobolevSpace.value P u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (y : EulerLiftedGradientSpace.Vector3) (θ : ℝ) : (EulerSobolevPointEvaluation.pointEvaluation P (y, ↑θ)) ((sobolevAverage P 3) u) = P⁻¹ • ∫ (s : ℝ) in 0..P, f (y, ↑s)

Pointwise identification with the actual normalized angular integral, at every angle.

theorem EulerCylinderAngleAverage.average_eq_zero_iff (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : Continuous f) (hrep : ↑↑(EulerCylinderSobolevSpace.value P u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) : (average P) (EulerCylinderSobolevSpace.value P u) = 0 ↔ ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0

The operator's zero kernel is precisely the classical zero-mean condition.