Bounded linear images of genuine uniformly smooth coefficient paths.

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.map {K : Type u_1} {V : Type u_2} {W : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : SmoothCoefficientPath K V) : SmoothCoefficientPath K W

Apply a fixed bounded linear map to the actual field and all its literal derivative jets.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerMeanCoefficients.SmoothCoefficientPath.map_apply {K : Type u_1} {V : Type u_2} {W : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : SmoothCoefficientPath K V) (t : K) (x : EulerSmoothLimit.Space) : ((map L A).field t) x = L ((A.field t) x)

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

Contraction of coefficient values preserves every actual spatial derivative bound.