Actual angular means of the reconstructed continuous-time cylinder fields.

theorem EulerCylinderAngleAverage.pointField_mean_zero_iff (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) : (average P) (p t) = 0 ↔ ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, EulerCylinderSmoothOrbit.pointField P p hp t (y, ↑s) = 0

The actual L² kernel condition and the literal classical mean agree at every time.

theorem EulerCylinderAngleAverage.pathAverage_eq_zero_iff (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : (pathAverage P) p = 0 ↔ ∀ (t : K) (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, EulerCylinderSmoothOrbit.pointField P p hp t (y, ↑s) = 0

theorem EulerCylinderAngleAverage.pathAverage_orbit_contDiff (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((pathAverage P) p)