Actual angular averaging on the cylinder, including its supported spaces.

noncomputable def EulerCylinderAngleAverage.angleCurve (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) (s : ℝ) : ↥(EulerLpCylinderTranslation.CylinderL2 P V)

Angle curve, given by translate P (0,s) u.

Equations

• EulerCylinderAngleAverage.angleCurve P u s = (EulerLpCylinderTranslation.translate P (0, s)) u

theorem EulerCylinderAngleAverage.angleCurve_continuous (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : Continuous (angleCurve P u)

noncomputable def EulerCylinderAngleAverage.averageIntegral (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : ↥(EulerLpCylinderTranslation.CylinderL2 P V)

Average integral, given by P⁻¹ • (∫ s in (0 : ℝ)..P, angleCurve P u s).

Equations

• EulerCylinderAngleAverage.averageIntegral P u = P⁻¹ • ∫ (s : ℝ) in 0..P, EulerCylinderAngleAverage.angleCurve P u s

theorem EulerCylinderAngleAverage.averageIntegral_add (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : averageIntegral P (u + v) = averageIntegral P u + averageIntegral P v

theorem EulerCylinderAngleAverage.averageIntegral_smul (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (r : ℝ) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : averageIntegral P (r • u) = r • averageIntegral P u

theorem EulerCylinderAngleAverage.averageIntegral_norm (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : ‖averageIntegral P u‖ ≤ ‖u‖

noncomputable def EulerCylinderAngleAverage.averageLinear (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : ↥(EulerLpCylinderTranslation.CylinderL2 P V) →ₗ[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V)

Average linear, bundling toFun, map_add, map_smul.

Equations

• EulerCylinderAngleAverage.averageLinear P = { toFun := EulerCylinderAngleAverage.averageIntegral P, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerCylinderAngleAverage.average (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : ↥(EulerLpCylinderTranslation.CylinderL2 P V) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V)

The Bochner average of genuine angular translations.

Equations

• EulerCylinderAngleAverage.average P = (EulerCylinderAngleAverage.averageLinear P).mkContinuous 1 ⋯

@[simp]

theorem EulerCylinderAngleAverage.average_apply (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : (average P) u = averageIntegral P u

theorem EulerCylinderAngleAverage.average_norm (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : ‖average P‖ ≤ 1

theorem EulerCylinderAngleAverage.average_translation (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (a : EulerLiftedGradientSpace.LiftTangent) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : (average P) ((EulerLpCylinderTranslation.translate P a) u) = (EulerLpCylinderTranslation.translate P a) ((average P) u)

noncomputable def EulerCylinderAngleAverage.pathAverage (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))

Path average, given by (average P).compLeftContinuous ℝ K.

Equations

• EulerCylinderAngleAverage.pathAverage P = ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderAngleAverage.average P)

@[simp]

theorem EulerCylinderAngleAverage.pathAverage_apply (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))) (t : K) : ((pathAverage P) u) t = (average P) (u t)

theorem EulerCylinderAngleAverage.pathAverage_norm (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] [CompactSpace K] : ‖pathAverage P‖ ≤ 1

theorem EulerCylinderAngleAverage.pathAverage_translation (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {K : Type u_2} [TopologicalSpace K] (a : EulerLiftedGradientSpace.LiftTangent) (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))) : (pathAverage P) ((EulerLpCylinderTranslation.pathTranslate P a) u) = (EulerLpCylinderTranslation.pathTranslate P a) ((pathAverage P) u)

theorem EulerCylinderAngleAverage.average_intertwines (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (L : ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F)) (hL : ∀ (s : ℝ) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)), L ((EulerLpCylinderTranslation.translate P (0, s)) u) = (EulerLpCylinderTranslation.translate P (0, s)) (L u)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)) : (average P) (L u) = L ((average P) u)

Every actual angular intertwiner commutes with the constructed average.

theorem EulerCylinderAngleAverage.average_fullOperator (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (A : BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)) : (average P) (((EulerLpCylinderRectangular.fullOperatorMap P) A) u) = ((EulerLpCylinderRectangular.fullOperatorMap P) A) ((average P) u)

Spatial rectangular coefficients preserve angular means exactly.

theorem EulerCylinderAngleAverage.pathAverage_fullMultiplier (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {K : Type u_3} [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P E))) : (pathAverage P) (((EulerLpCylinderRectangular.fullMultiplierMap P) A) u) = ((EulerLpCylinderRectangular.fullMultiplierMap P) A) ((pathAverage P) u)

theorem EulerCylinderAngleAverage.average_mem (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (u : ↥(EulerLpCylinderPaths.Supported P V S hS)) : (average P) ↑u ∈ EulerLpCylinderPaths.Supported P V S hS

Angular averaging preserves the actual spatial support subspace.

noncomputable def EulerCylinderAngleAverage.supportedAverage (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : ↥(EulerLpCylinderPaths.Supported P V S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported P V S hS)

Supported average, given by ((average P).comp (Supported P V S hS).subtypeL).codRestrict (Supported P V S hS) (average_mem P S hS).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerCylinderAngleAverage.supportedAverage_coe (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (u : ↥(EulerLpCylinderPaths.Supported P V S hS)) : ↑((supportedAverage P S hS) u) = (average P) ↑u

theorem EulerCylinderAngleAverage.supportedAverage_norm (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : ‖supportedAverage P S hS‖ ≤ 1