A genuine bounded cylinder-to-spatial mean, defined by the adjoint of constant extension.

theorem EulerCylinderSpatialMean.embedding_translate (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (a : EulerLiftedGradientSpace.LiftTangent) (u : ↥(EulerCylinderSpatialEmbedding.SpatialL2 V)) : (EulerLpCylinderTranslation.translate P a) ((EulerCylinderSpatialEmbedding.embedding P) u) = (EulerCylinderSpatialEmbedding.embedding P) ((EulerLpTranslation.translation a.1) u)

noncomputable def EulerCylinderSpatialMean.mean (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] : ↥(EulerLpCylinderTranslation.CylinderL2 P V) →L[ℝ] ↥(EulerCylinderSpatialEmbedding.SpatialL2 V)

Mean, given by P⁻¹ • (embedding P).adjoint.

Equations

• EulerCylinderSpatialMean.mean P = P⁻¹ • ContinuousLinearMap.adjoint (EulerCylinderSpatialEmbedding.embedding P)

@[simp]

theorem EulerCylinderSpatialMean.mean_apply (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : (mean P) u = P⁻¹ • (ContinuousLinearMap.adjoint (EulerCylinderSpatialEmbedding.embedding P)) u

theorem EulerCylinderSpatialMean.mean_norm (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] : ‖mean P‖ ≤ P⁻¹ * √P

theorem EulerCylinderSpatialMean.mean_embedding (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (u : ↥(EulerCylinderSpatialEmbedding.SpatialL2 V)) : (mean P) ((EulerCylinderSpatialEmbedding.embedding P) u) = u

theorem EulerCylinderSpatialMean.cylinder_translation_inner (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (a : EulerLiftedGradientSpace.LiftTangent) (u v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : inner ℝ ((EulerLpCylinderTranslation.translate P a) u) v = inner ℝ u ((EulerLpCylinderTranslation.translate P (-a)) v)

theorem EulerCylinderSpatialMean.spatial_translation_inner {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (a : EulerSmoothLimit.Space) (u v : ↥(EulerCylinderSpatialEmbedding.SpatialL2 V)) : inner ℝ ((EulerLpTranslation.translation a) u) v = inner ℝ u ((EulerLpTranslation.translation (-a)) v)

theorem EulerCylinderSpatialMean.mean_translate (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (a : EulerLiftedGradientSpace.LiftTangent) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : (mean P) ((EulerLpCylinderTranslation.translate P a) u) = (EulerLpTranslation.translation a.1) ((mean P) u)

The bounded mean commutes with actual spatial translations and removes angular translations.

theorem EulerCylinderSpatialMean.mean_average (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : (mean P) ((EulerCylinderAngleAverage.average P) u) = (mean P) u

Averaging over the angular translations does not change the actual spatial mean.