Spatial translation calculus for coefficients uniformly on a compact time interval.

@[instance_reducible]

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

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

Equations

• EulerMeanCoefficients.instMeanCoefficientPath1 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanCoefficients.instMeanCoefficientPath2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientPath3 {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))

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

Equations

• EulerMeanCoefficients.instMeanCoefficientPath3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientPath4 {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))

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

Equations

• EulerMeanCoefficients.instMeanCoefficientPath4 = inferInstance

noncomputable def EulerMeanCoefficients.translateCoefficientPath {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (a : EulerSmoothLimit.Space) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)

Translate coefficient path as an element of C(K, Space →ᵇ V).

Equations

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

@[simp]

theorem EulerMeanCoefficients.translateCoefficientPath_apply {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (a : EulerSmoothLimit.Space) (t : K) : (translateCoefficientPath A a) t = translated (A t) a

noncomputable def EulerMeanCoefficients.pathDirection {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))) (a : EulerSmoothLimit.Space) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)

Path direction, given by ⟨fun t => fieldDerivativeMap (DA t) a, ((derivativeBundling (V := V)).continuous.comp DA.continuous).clm_apply continuous_const⟩.

Equations

• EulerMeanCoefficients.pathDirection DA a = { toFun := fun (t : K) => (EulerMeanCoefficients.fieldDerivativeMap (DA t)) a, continuous_toFun := ⋯ }

@[simp]

theorem EulerMeanCoefficients.pathDirection_apply {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))) (a : EulerSmoothLimit.Space) (t : K) (x : EulerSmoothLimit.Space) : ((pathDirection DA a) t) x = ((DA t) x) a

theorem EulerMeanCoefficients.pathDirection_norm_le {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))) (a : EulerSmoothLimit.Space) : ‖pathDirection DA a‖ ≤ ‖DA‖ * ‖a‖

noncomputable def EulerMeanCoefficients.pathDerivativeLinear {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))) : EulerSmoothLimit.Space →ₗ[ℝ] C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)

Path derivative linear, bundling toFun, map_add, map_smul.

Equations

• EulerMeanCoefficients.pathDerivativeLinear DA = { toFun := EulerMeanCoefficients.pathDirection DA, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerMeanCoefficients.pathDerivativeMap {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))) : EulerSmoothLimit.Space →L[ℝ] C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)

Path derivative map, bundling toLinearMap, cont.

Equations

• EulerMeanCoefficients.pathDerivativeMap DA = { toLinearMap := EulerMeanCoefficients.pathDerivativeLinear DA, cont := ⋯ }

@[simp]

theorem EulerMeanCoefficients.pathDerivativeMap_apply {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))) (a : EulerSmoothLimit.Space) (t : K) (x : EulerSmoothLimit.Space) : (((pathDerivativeMap DA) a) t) x = ((DA t) x) a

theorem EulerMeanCoefficients.pathDerivativeMap_norm_le {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))) : ‖pathDerivativeMap DA‖ ≤ ‖DA‖

noncomputable def EulerMeanCoefficients.pathDerivativeBundlingLinear {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V)) →ₗ[ℝ] EulerSmoothLimit.Space →L[ℝ] C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)

Path derivative bundling linear, bundling toFun, map_add, map_smul.

Equations

• EulerMeanCoefficients.pathDerivativeBundlingLinear = { toFun := EulerMeanCoefficients.pathDerivativeMap, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerMeanCoefficients.pathDerivativeBundling {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V)) →L[ℝ] EulerSmoothLimit.Space →L[ℝ] C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)

Path derivative bundling, bundling toLinearMap, cont.

Equations

• EulerMeanCoefficients.pathDerivativeBundling = { toLinearMap := EulerMeanCoefficients.pathDerivativeBundlingLinear, cont := ⋯ }

theorem EulerMeanCoefficients.translateCoefficientPath_taylor {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (DA : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))) (hA : ∀ (t : K), ContDiff ℝ ↑⊤ ⇑(A t)) (hDA : ∀ (t : K) (x : EulerSmoothLimit.Space), (DA t) x = fderiv ℝ (⇑(A t)) x) (M : ℝ) (hM : 0 ≤ M) (h₂ : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ ⇑(A t)) x‖ ≤ M) (a b : EulerSmoothLimit.Space) : ‖translateCoefficientPath A b - translateCoefficientPath A a - (pathDerivativeMap (translateCoefficientPath DA a)) (b - a)‖ ≤ M * ‖b - a‖ ^ 2

theorem EulerMeanCoefficients.translateCoefficientPath_hasFDerivAt {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (DA : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))) (hA : ∀ (t : K), ContDiff ℝ ↑⊤ ⇑(A t)) (hDA : ∀ (t : K) (x : EulerSmoothLimit.Space), (DA t) x = fderiv ℝ (⇑(A t)) x) (M : ℝ) (hM : 0 ≤ M) (h₂ : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ ⇑(A t)) x‖ ≤ M) (a : EulerSmoothLimit.Space) : HasFDerivAt (translateCoefficientPath A) (pathDerivativeMap (translateCoefficientPath DA a)) a

Actual spatial differentiation holds in the uniform time-path norm.

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientPath5 : NormedAddCommGroup Field

Cache the standard NormedAddCommGroup Field instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instMeanCoefficientPath5 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientPath6 : NormedSpace ℝ Field

Cache the standard NormedSpace ℝ Field instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instMeanCoefficientPath6 = inferInstance

@[reducible, inline]

noncomputable abbrev EulerMeanCoefficients.translatedPath (T : ℝ) (A : C(↑(Set.Icc 0 T), Field)) (a : EulerSmoothLimit.Space) : C(↑(Set.Icc 0 T), Field)

Translated path: an abbreviation for translateCoefficientPath A a.

Equations

• EulerMeanCoefficients.translatedPath T A a = EulerMeanCoefficients.translateCoefficientPath A a

@[simp]

theorem EulerMeanCoefficients.translatedPath_apply (T : ℝ) (A : C(↑(Set.Icc 0 T), Field)) (a : EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ((translatedPath T A a) t) x = (A t) (x + a)