All-order spatial translation regularity uniformly over a compact parameter interval.

@[instance_reducible]

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

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

Equations

• EulerMeanCoefficients.instSmoothCoefficientPath1 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanCoefficients.instSmoothCoefficientPath2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instSmoothCoefficientPath3 {W : Type w} [NormedAddCommGroup W] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space W)

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

Equations

• EulerMeanCoefficients.instSmoothCoefficientPath3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instSmoothCoefficientPath4 {W : Type w} [NormedAddCommGroup W] [NormedSpace ℝ W] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space W)

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

Equations

• EulerMeanCoefficients.instSmoothCoefficientPath4 = inferInstance

noncomputable def EulerMeanCoefficients.mapCoefficientPath {K : Type u} [TopologicalSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] {W : Type w} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V) →L[ℝ] C(K, BoundedContinuousFunction EulerSmoothLimit.Space W)

Map coefficient path, given by (L.compLeftContinuousBounded Space).compLeftContinuous ℝ K.

Equations

• EulerMeanCoefficients.mapCoefficientPath L = ContinuousLinearMap.compLeftContinuous ℝ K (ContinuousLinearMap.compLeftContinuousBounded EulerSmoothLimit.Space L)

@[simp]

theorem EulerMeanCoefficients.mapCoefficientPath_apply {K : Type u} [TopologicalSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] {W : Type w} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (t : K) (x : EulerSmoothLimit.Space) : (((mapCoefficientPath L) A) t) x = L ((A t) x)

structure EulerMeanCoefficients.SmoothCoefficientPath (K : Type u) [TopologicalSpace K] [CompactSpace K] (V : Type v) [NormedAddCommGroup V] [NormedSpace ℝ V] : Type (max u v)

Actual coefficient jets, continuous in the uniform time-path norm at every fixed spatial order.

• field : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)

  Underlying field of SmoothCoefficientPath, with values in C(K, Space →ᵇ V).

• smooth (t : K) : ContDiff ℝ ↑⊤ ⇑(self.field t)
• jet (n : ℕ) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] V))

  Jet of SmoothCoefficientPath, of type (n : ℕ) → C(K, Space →ᵇ (Space [×n]→L[ℝ] V)).

• jet_eq (n : ℕ) (t : K) (x : EulerSmoothLimit.Space) : ((self.jet n) t) x = iteratedFDeriv ℝ n (⇑(self.field t)) x

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instSmoothCoefficientPath5 {V : Type v} [NormedAddCommGroup V] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space V)

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

Equations

• EulerMeanCoefficients.SmoothCoefficientPath.instSmoothCoefficientPath5 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instSmoothCoefficientPath6 {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space V)

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

Equations

• EulerMeanCoefficients.SmoothCoefficientPath.instSmoothCoefficientPath6 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instSmoothCoefficientPath7 {V : Type v} [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.SmoothCoefficientPath.instSmoothCoefficientPath7 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instSmoothCoefficientPath8 {V : Type v} [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.SmoothCoefficientPath.instSmoothCoefficientPath8 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instSmoothCoefficientPath9 {V : Type v} [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.SmoothCoefficientPath.instSmoothCoefficientPath9 n = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instSmoothCoefficientPath10 {V : Type v} [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.SmoothCoefficientPath.instSmoothCoefficientPath10 n = inferInstance

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.derivativeField {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))

Derivative field, given by mapCoefficientPath (continuousMultilinearCurryFin1 ℝ Space V).toContinuousLinearEquiv.toContinuousLinearMap (A.jet 1).

Equations

• A.derivativeField = (EulerMeanCoefficients.mapCoefficientPath ↑↑(continuousMultilinearCurryFin1 ℝ EulerSmoothLimit.Space V)) (A.jet 1)

theorem EulerMeanCoefficients.SmoothCoefficientPath.derivativeField_eq {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (t : K) (x : EulerSmoothLimit.Space) : (A.derivativeField t) x = fderiv ℝ (⇑(A.field t)) x

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.derivativeJet {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (n : ℕ) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space →L[ℝ] V))

Derivative jet, constructed using mapCoefficientPath.

Equations

• A.derivativeJet n = (EulerMeanCoefficients.mapCoefficientPath ↑↑(continuousMultilinearCurryRightEquiv' ℝ n EulerSmoothLimit.Space V)) (A.jet (n + 1))

theorem EulerMeanCoefficients.SmoothCoefficientPath.derivativeJet_eq {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (n : ℕ) (t : K) (x : EulerSmoothLimit.Space) : ((A.derivativeJet n) t) x = iteratedFDeriv ℝ n (fderiv ℝ ⇑(A.field t)) x

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.derivative {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) : SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] V)

Derivative, bundling field, smooth, fderiv, exact and the required compatibility proofs.

Equations

• A.derivative = { field := A.derivativeField, smooth := ⋯, jet := A.derivativeJet, jet_eq := ⋯ }

theorem EulerMeanCoefficients.SmoothCoefficientPath.translation_hasFDerivAt {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (a : EulerSmoothLimit.Space) : HasFDerivAt (translateCoefficientPath A.field) (pathDerivativeMap (translateCoefficientPath A.derivative.field a)) a

theorem EulerMeanCoefficients.SmoothCoefficientPath.translation_fderiv {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) : fderiv ℝ (translateCoefficientPath A.field) = fun (a : EulerSmoothLimit.Space) => pathDerivativeBundling (translateCoefficientPath A.derivative.field a)

theorem EulerMeanCoefficients.SmoothCoefficientPath.translation_contDiff {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) : ContDiff ℝ (↑⊤) (translateCoefficientPath A.field)

Smoothness in the spatial translation parameter holds in the uniform time-path topology.