Fixed bounded maps on actual cylinder L² classes and continuous paths.

noncomputable def EulerCylinderConstantMap.map (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) : ↥(EulerLpCylinderTranslation.CylinderL2 period E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 period F)

Map, given by L.compLpL 2 (liftMeasure period).

Equations

• EulerCylinderConstantMap.map period L = ContinuousLinearMap.compLpL 2 (EulerLiftedGradientSpace.liftMeasure period) L

theorem EulerCylinderConstantMap.map_ae (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) (u : ↥(EulerLpCylinderTranslation.CylinderL2 period E)) : ↑↑((map period L) u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => L (↑↑u x)

theorem EulerCylinderConstantMap.map_norm (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) : ‖map period L‖ ≤ ‖L‖

theorem EulerCylinderConstantMap.map_comp (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (L : F →L[ℝ] G) (M : E →L[ℝ] F) : map period (L ∘SL M) = map period L ∘SL map period M

@[simp]

theorem EulerCylinderConstantMap.map_id (period : ℝ) [Fact (0 < period)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : map period (ContinuousLinearMap.id ℝ E) = ContinuousLinearMap.id ℝ ↥(EulerLpCylinderTranslation.CylinderL2 period E)

theorem EulerCylinderConstantMap.map_translation (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) (a : EulerLiftedGradientSpace.LiftTangent) (u : ↥(EulerLpCylinderTranslation.CylinderL2 period E)) : (map period L) ((EulerLpCylinderTranslation.translate period a) u) = (EulerLpCylinderTranslation.translate period a) ((map period L) u)

noncomputable def EulerCylinderConstantMap.pathMap (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_4} [TopologicalSpace K] (L : E →L[ℝ] F) : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period F))

Path map, given by (map period L).compLeftContinuous ℝ K.

Equations

• EulerCylinderConstantMap.pathMap period L = ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderConstantMap.map period L)

@[simp]

theorem EulerCylinderConstantMap.pathMap_apply (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_4} [TopologicalSpace K] (L : E →L[ℝ] F) (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))) (t : K) : ((pathMap period L) u) t = (map period L) (u t)

theorem EulerCylinderConstantMap.pathMap_norm (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_4} [TopologicalSpace K] [CompactSpace K] (L : E →L[ℝ] F) : ‖pathMap period L‖ ≤ ‖L‖

theorem EulerCylinderConstantMap.pathMap_translation (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_4} [TopologicalSpace K] (L : E →L[ℝ] F) (a : EulerLiftedGradientSpace.LiftTangent) (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))) : (pathMap period L) ((EulerLpCylinderTranslation.pathTranslate period a) u) = (EulerLpCylinderTranslation.pathTranslate period a) ((pathMap period L) u)

theorem EulerCylinderConstantMap.pathMap_orbit_contDiff (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_4} [TopologicalSpace K] [CompactSpace K] (L : E →L[ℝ] F) (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) u) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((pathMap period L) u)