Profile normalization across the history/forward junction #
The profile is exactly one on the history interval and the specified positive continuous profile on the elapsed forward interval. Normalization commutes with the actual join, without estimating either extremum of the profile.
noncomputable def
EulerElapsedTimePathGluing.profile
(S τ : ℝ)
(hτ0 : 0 ≤ τ)
(hτS : τ ≤ S)
(g : C(↑(Set.Icc 0 (S - τ)), ℝ))
(hg0 : g ⟨0, ⋯⟩ = 1)
:
The literal piecewise profile; no differentiability of it is required.
Equations
- EulerElapsedTimePathGluing.profile S τ hτ0 hτS g hg0 = EulerElapsedTimePathGluing.join S τ hτ0 hτS (ContinuousMap.const (↑(Set.Icc 0 τ)) 1) g ⋯
Instances For
theorem
EulerElapsedTimePathGluing.normalize_match
(S τ : ℝ)
(hτ0 : 0 ≤ τ)
(hτS : τ ≤ S)
(g : C(↑(Set.Icc 0 (S - τ)), ℝ))
(hg0 : g ⟨0, ⋯⟩ = 1)
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(hg : ∀ (t : ↑(Set.Icc 0 (S - τ))), 0 < g t)
(u : C(↑(Set.Icc 0 τ), E))
(v : C(↑(Set.Icc 0 (S - τ)), E))
(hm : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩)
:
theorem
EulerElapsedTimePathGluing.normalize_join
(S τ : ℝ)
(hτ0 : 0 ≤ τ)
(hτS : τ ≤ S)
(g : C(↑(Set.Icc 0 (S - τ)), ℝ))
(hg0 : g ⟨0, ⋯⟩ = 1)
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(hg : ∀ (t : ↑(Set.Icc 0 (S - τ))), 0 < g t)
(u : C(↑(Set.Icc 0 τ), E))
(v : C(↑(Set.Icc 0 (S - τ)), E))
(hm : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩)
:
(EulerContinuousTimeWeight.normalize (profile S τ hτ0 hτS g hg0) ⋯) (join S τ hτ0 hτS u v hm) = join S τ hτ0 hτS u ((EulerContinuousTimeWeight.normalize g hg) v) ⋯
The normalized join is exactly the join of the normalized forward path.
theorem
EulerElapsedTimePathGluing.normalize_initial
(S τ : ℝ)
(hτ0 : 0 ≤ τ)
(hτS : τ ≤ S)
(g : C(↑(Set.Icc 0 (S - τ)), ℝ))
(hg0 : g ⟨0, ⋯⟩ = 1)
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(hg : ∀ (t : ↑(Set.Icc 0 (S - τ))), 0 < g t)
(p : C(↑(Set.Icc 0 S), E))
:
((EulerContinuousTimeWeight.normalize (profile S τ hτ0 hτS g hg0) ⋯) p).comp
(EulerTimeIntervalRestriction.initialInclusion S τ hτS) = p.comp (EulerTimeIntervalRestriction.initialInclusion S τ hτS)
Restriction of a normalized full path to the history is unchanged.
theorem
EulerElapsedTimePathGluing.normalize_tail
(S τ : ℝ)
(hτ0 : 0 ≤ τ)
(hτS : τ ≤ S)
(g : C(↑(Set.Icc 0 (S - τ)), ℝ))
(hg0 : g ⟨0, ⋯⟩ = 1)
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(hg : ∀ (t : ↑(Set.Icc 0 (S - τ))), 0 < g t)
(p : C(↑(Set.Icc 0 S), E))
:
((EulerContinuousTimeWeight.normalize (profile S τ hτ0 hτS g hg0) ⋯) p).comp
(EulerTimeIntervalRestriction.tailInclusion S τ hτ0) = (EulerContinuousTimeWeight.normalize g hg) (p.comp (EulerTimeIntervalRestriction.tailInclusion S τ hτ0))
Restriction of the normalized full path to the future uses exactly g.
theorem
EulerLpCylinderTranslation.normalize_orbit_contDiff
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
{K : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
(g : C(K, ℝ))
(hg : ∀ (t : K), 0 < g t)
(p : C(K, ↥(CylinderL2 P V)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) p)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) p)
theorem
EulerLpCylinderTranslation.normalized_join_block
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(S τ : ℝ)
(hτ0 : 0 ≤ τ)
(hτS : τ ≤ S)
(g : C(↑(Set.Icc 0 (S - τ)), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 (S - τ))), 0 < g t)
(hg0 : g ⟨0, ⋯⟩ = 1)
(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)
((EulerContinuousTimeWeight.normalize (EulerElapsedTimePathGluing.profile S τ hτ0 hτS g hg0) ⋯)
(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) ((EulerContinuousTimeWeight.normalize g hg) v))
n a
Profile normalization at the join preserves the exact external radius.