Bounded spatial maps and mixed derivative words commute with the actual elapsed-time join.
theorem
EulerElapsedTimePathGluing.join_map
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(S τ : ℝ)
(hτ0 : 0 ≤ τ)
(hτS : τ ≤ S)
(u : C(↑(Set.Icc 0 τ), E))
(v : C(↑(Set.Icc 0 (S - τ)), E))
(hm : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩)
(L : E →L[ℝ] F)
:
(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 S)) L) (join S τ hτ0 hτS u v hm) = join S τ hτ0 hτS ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 τ)) L) u)
((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 (S - τ))) L) v) ⋯
theorem
EulerLpCylinderTranslation.join_translation
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(S τ : ℝ)
(hτ0 : 0 ≤ τ)
(hτS : τ ≤ S)
(u : C(↑(Set.Icc 0 τ), ↥(CylinderL2 P V)))
(v : C(↑(Set.Icc 0 (S - τ)), ↥(CylinderL2 P V)))
(hm : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩)
(a : EulerLiftedGradientSpace.LiftTangent)
:
(pathTranslate P a) (EulerElapsedTimePathGluing.join S τ hτ0 hτS u v hm) = EulerElapsedTimePathGluing.join S τ hτ0 hτS ((pathTranslate P a) u) ((pathTranslate P a) v) ⋯
theorem
EulerLpCylinderTranslation.join_orbit_contDiff
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(S τ : ℝ)
(hτ0 : 0 ≤ τ)
(hτS : τ ≤ S)
(u : C(↑(Set.Icc 0 τ), ↥(CylinderL2 P V)))
(v : C(↑(Set.Icc 0 (S - τ)), ↥(CylinderL2 P V)))
(hm : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩)
(hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) u)
(hv : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) v)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(pathTranslate P a) (EulerElapsedTimePathGluing.join S τ hτ0 hτS u v hm)
theorem
EulerLpCylinderTranslation.join_orbit_block
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(S τ : ℝ)
(hτ0 : 0 ≤ τ)
(hτS : τ ≤ S)
(u : C(↑(Set.Icc 0 τ), ↥(CylinderL2 P V)))
(v : C(↑(Set.Icc 0 (S - τ)), ↥(CylinderL2 P V)))
(hm : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩)
(hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) u)
(hv : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) v)
{ι : Type u_2}
[Fintype ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(q n : ℕ)
(a : EulerLiftedGradientSpace.LiftTangent)
:
EulerParameterWordGevrey.block directions q
(fun (b : EulerLiftedGradientSpace.LiftTangent) =>
(pathTranslate P b) (EulerElapsedTimePathGluing.join S τ hτ0 hτS u v hm))
n a ≤ EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P b) u)
n a + EulerParameterWordGevrey.block directions q
(fun (b : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P b) v) n a