Restricting the time parameter of genuine smooth coefficient fields

Continuous precomposition keeps the actual spatial jets and has norm at most one. In particular it does not enlarge the spatial factorial radius when a source field is restricted to a history interval or shifted to a forward interval.

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instSmoothCoefficientTimeRestriction1 {V : Type u_3} [NormedAddCommGroup V] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space V)

Cache the standard NormedAddCommGroup (Space →ᵇ V) instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instSmoothCoefficientTimeRestriction1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instSmoothCoefficientTimeRestriction2 {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space V)

Cache the standard NormedSpace ℝ (Space →ᵇ V) instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instSmoothCoefficientTimeRestriction2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instSmoothCoefficientTimeRestriction3 {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] V))

Cache the standard NormedAddCommGroup (Space →ᵇ (Space [×n]→L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instSmoothCoefficientTimeRestriction3 n = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instSmoothCoefficientTimeRestriction4 {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] V))

Cache the standard NormedSpace ℝ (Space →ᵇ (Space [×n]→L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instSmoothCoefficientTimeRestriction4 n = inferInstance

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.comp {K : Type u_1} {L : Type u_2} {V : Type u_3} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (φ : C(L, K)) : SmoothCoefficientPath L V

Actual time precomposition, including every spatial jet.

Equations

• A.comp φ = { field := A.field.comp φ, smooth := ⋯, jet := fun (n : ℕ) => (A.jet n).comp φ, jet_eq := ⋯ }

@[simp]

theorem EulerMeanCoefficients.SmoothCoefficientPath.comp_apply {K : Type u_1} {L : Type u_2} {V : Type u_3} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (φ : C(L, K)) (t : L) (x : EulerSmoothLimit.Space) : ((A.comp φ).field t) x = (A.field (φ t)) x

theorem EulerMeanCoefficients.SmoothCoefficientPath.comp_norm_le {K : Type u_1} {L : Type u_2} {V : Type u_3} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (φ : C(L, K)) : ‖(A.comp φ).field‖ ≤ ‖A.field‖

theorem EulerMeanCoefficients.SmoothCoefficientPath.comp_jet_norm_le {K : Type u_1} {L : Type u_2} {V : Type u_3} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (φ : C(L, K)) (n : ℕ) : ‖(A.comp φ).jet n‖ ≤ ‖A.jet n‖

theorem EulerMeanCoefficients.SmoothCoefficientPath.comp_translation {K : Type u_1} {L : Type u_2} {V : Type u_3} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (φ : C(L, K)) (a : EulerSmoothLimit.Space) : translateCoefficientPath (A.comp φ).field a = (translateCoefficientPath A.field a).comp φ

theorem EulerMeanCoefficients.SmoothCoefficientPath.comp_derivative_bound {K : Type u_1} {L : Type u_2} {V : Type u_3} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (φ : C(L, K)) (n : ℕ) (C : ℝ) (hb : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(A.field t)) x‖ ≤ C) (t : L) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑((A.comp φ).field t)) x‖ ≤ C

A continuous change of time parameter preserves each literal spatial derivative bound with exactly the same constant.

theorem EulerMeanCoefficients.SmoothCoefficientPath.comp_translation_bound {K : Type u_1} {L : Type u_2} {V : Type u_3} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (φ : C(L, K)) (n : ℕ) (C : ℝ) (hC : 0 ≤ C) (hb : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(A.field t)) x‖ ≤ C) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (translateCoefficientPath (A.comp φ).field) a‖ ≤ C

def EulerTimeIntervalRestriction.initialInclusion (S τ : ℝ) (hτS : τ ≤ S) : C(↑(Set.Icc 0 τ), ↑(Set.Icc 0 S))

Initial inclusion, given by ⟨fun t => ⟨t,t.property.1,t.property.2.trans hτS⟩, continuous_subtype_val.subtype_mk _⟩.

Equations

• EulerTimeIntervalRestriction.initialInclusion S τ hτS = { toFun := fun (t : ↑(Set.Icc 0 τ)) => ⟨↑t, ⋯⟩, continuous_toFun := ⋯ }

def EulerTimeIntervalRestriction.tailInclusion (S τ : ℝ) (hτ : 0 ≤ τ) : C(↑(Set.Icc 0 (S - τ)), ↑(Set.Icc 0 S))

Tail inclusion, given by ⟨fun t => ⟨τ+t,add_nonneg hτ t.property.1,by linarith [t.property.2]⟩, (continuous_const.add continuous_subtype_val).subtype_mk _⟩.

Equations

• EulerTimeIntervalRestriction.tailInclusion S τ hτ = { toFun := fun (t : ↑(Set.Icc 0 (S - τ))) => ⟨τ + ↑t, ⋯⟩, continuous_toFun := ⋯ }

def EulerTimeIntervalRestriction.initialPath {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (S τ : ℝ) (hτS : τ ≤ S) : C(↑(Set.Icc 0 S), V) →L[ℝ] C(↑(Set.Icc 0 τ), V)

Initial path, given by ContinuousMap.compCLM ℝ V (initialInclusion S τ hτS).

Equations

• EulerTimeIntervalRestriction.initialPath S τ hτS = ContinuousMap.compCLM ℝ V (EulerTimeIntervalRestriction.initialInclusion S τ hτS)

def EulerTimeIntervalRestriction.tailPath {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (S τ : ℝ) (hτ : 0 ≤ τ) : C(↑(Set.Icc 0 S), V) →L[ℝ] C(↑(Set.Icc 0 (S - τ)), V)

Tail path, given by ContinuousMap.compCLM ℝ V (tailInclusion S τ hτ).

Equations

• EulerTimeIntervalRestriction.tailPath S τ hτ = ContinuousMap.compCLM ℝ V (EulerTimeIntervalRestriction.tailInclusion S τ hτ)

theorem EulerTimeIntervalRestriction.initialPath_norm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (S τ : ℝ) (hτS : τ ≤ S) : ‖initialPath S τ hτS‖ ≤ 1

theorem EulerTimeIntervalRestriction.tailPath_norm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (S τ : ℝ) (hτ : 0 ≤ τ) : ‖tailPath S τ hτ‖ ≤ 1

theorem EulerTimeIntervalRestriction.initial_extend {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (S τ : ℝ) (hS : 0 ≤ S) (hτ : 0 ≤ τ) (hτS : τ ≤ S) (A : C(↑(Set.Icc 0 S), V)) (t : ℝ) (ht : t ∈ Set.Icc 0 τ) : EulerVolterraConvolution.extendPath τ hτ ((initialPath S τ hτS) A) t = EulerVolterraConvolution.extendPath S hS A t

theorem EulerTimeIntervalRestriction.tail_extend {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (S τ : ℝ) (hS : 0 ≤ S) (hτ : 0 ≤ τ) (hτS : τ ≤ S) (A : C(↑(Set.Icc 0 S), V)) (t : ℝ) (ht : t ∈ Set.Icc 0 (S - τ)) : EulerVolterraConvolution.extendPath (S - τ) ⋯ ((tailPath S τ hτ) A) t = EulerVolterraConvolution.extendPath S hS A (τ + t)

theorem EulerTimeIntervalRestriction.initialPath_hasDerivWithinAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (S τ : ℝ) (hS : 0 ≤ S) (hτ : 0 ≤ τ) (hτS : τ ≤ S) (A A₁ : C(↑(Set.Icc 0 S), V)) (hd : ∀ t ∈ Set.Icc 0 S, HasDerivWithinAt (EulerVolterraConvolution.extendPath S hS A) (EulerVolterraConvolution.extendPath S hS A₁ t) (Set.Icc 0 S) t) (t : ℝ) (ht : t ∈ Set.Icc 0 τ) : HasDerivWithinAt (EulerVolterraConvolution.extendPath τ hτ ((initialPath S τ hτS) A)) (EulerVolterraConvolution.extendPath τ hτ ((initialPath S τ hτS) A₁) t) (Set.Icc 0 τ) t

A true within-time derivative restricts to the closed history interval.

theorem EulerTimeIntervalRestriction.tailPath_hasDerivWithinAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (S τ : ℝ) (hS : 0 ≤ S) (hτ : 0 ≤ τ) (hτS : τ ≤ S) (A A₁ : C(↑(Set.Icc 0 S), V)) (hd : ∀ t ∈ Set.Icc 0 S, HasDerivWithinAt (EulerVolterraConvolution.extendPath S hS A) (EulerVolterraConvolution.extendPath S hS A₁ t) (Set.Icc 0 S) t) (t : ℝ) (ht : t ∈ Set.Icc 0 (S - τ)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath (S - τ) ⋯ ((tailPath S τ hτ) A)) (EulerVolterraConvolution.extendPath (S - τ) ⋯ ((tailPath S τ hτ) A₁) t) (Set.Icc 0 (S - τ)) t

Translation of the time variable has derivative one, including the within-derivatives at both ends of the forward interval.