Actual scalar time weighting commutes with cylinder inclusion, translations, and rectangular multiplication.
theorem
EulerLpCylinderRectangular.supportedMultiplier_weight
(period : ℝ)
[Fact (0 < period)]
{K : Type u_1}
{E : Type u_2}
{F : Type u_3}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
(S : Set EulerSmoothLimit.Space)
(hS : MeasurableSet S)
(g : C(K, ℝ))
(A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)))
(u : C(K, ↥(EulerLpCylinderPaths.Supported period E S hS)))
:
((supportedMultiplierMap period S hS) A) ((EulerContinuousTimeWeight.weight g) u) = (EulerContinuousTimeWeight.weight g) (((supportedMultiplierMap period S hS) A) u)
theorem
EulerLpCylinderRectangular.supportedMultiplier_normalize
(period : ℝ)
[Fact (0 < period)]
{K : Type u_1}
{E : Type u_2}
{F : Type u_3}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
(S : Set EulerSmoothLimit.Space)
(hS : MeasurableSet S)
(g : C(K, ℝ))
(hg : ∀ (t : K), 0 < g t)
(A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)))
(u : C(K, ↥(EulerLpCylinderPaths.Supported period E S hS)))
:
((supportedMultiplierMap period S hS) A) ((EulerContinuousTimeWeight.normalize g hg) u) = (EulerContinuousTimeWeight.normalize g hg) (((supportedMultiplierMap period S hS) A) u)
theorem
EulerLpCylinderRectangular.include_weight
(period : ℝ)
[Fact (0 < period)]
{K : Type u_1}
{E : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
(S : Set EulerSmoothLimit.Space)
(hS : MeasurableSet S)
(g : C(K, ℝ))
(u : C(K, ↥(EulerLpCylinderPaths.Supported period E S hS)))
:
(EulerLpCylinderPaths.includePath period S hS) ((EulerContinuousTimeWeight.weight g) u) = (EulerContinuousTimeWeight.weight g) ((EulerLpCylinderPaths.includePath period S hS) u)
theorem
EulerLpCylinderRectangular.include_normalize
(period : ℝ)
[Fact (0 < period)]
{K : Type u_1}
{E : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
(S : Set EulerSmoothLimit.Space)
(hS : MeasurableSet S)
(g : C(K, ℝ))
(hg : ∀ (t : K), 0 < g t)
(u : C(K, ↥(EulerLpCylinderPaths.Supported period E S hS)))
:
(EulerLpCylinderPaths.includePath period S hS) ((EulerContinuousTimeWeight.normalize g hg) u) = (EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderPaths.includePath period S hS) u)
theorem
EulerLpCylinderRectangular.translate_weight
(period : ℝ)
[Fact (0 < period)]
{K : Type u_1}
{E : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
(g : C(K, ℝ))
(a : EulerLiftedGradientSpace.LiftTangent)
(u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E)))
:
(EulerLpCylinderTranslation.pathTranslate period a) ((EulerContinuousTimeWeight.weight g) u) = (EulerContinuousTimeWeight.weight g) ((EulerLpCylinderTranslation.pathTranslate period a) u)
theorem
EulerLpCylinderRectangular.translate_normalize
(period : ℝ)
[Fact (0 < period)]
{K : Type u_1}
{E : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
(g : C(K, ℝ))
(hg : ∀ (t : K), 0 < g t)
(a : EulerLiftedGradientSpace.LiftTangent)
(u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E)))
:
(EulerLpCylinderTranslation.pathTranslate period a) ((EulerContinuousTimeWeight.normalize g hg) u) = (EulerContinuousTimeWeight.normalize g hg) ((EulerLpCylinderTranslation.pathTranslate period a) u)