A genuinely smooth bounded-coefficient translation orbit supplies actual bounded spatial derivatives, continuously over the time parameter.

@[instance_reducible]

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

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

Equations

• EulerMeanCoefficients.instCoefficientPathOrbit1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instCoefficientPathOrbit2 {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.instCoefficientPathOrbit2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanCoefficients.instCoefficientPathOrbit3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanCoefficients.instCoefficientPathOrbit4 = inferInstance

theorem EulerMeanCoefficients.coefficientOrbit_smooth {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (hA : ContDiff ℝ (↑⊤) (translateCoefficientPath A)) (t : K) : ContDiff ℝ ↑⊤ ⇑(A t)

theorem EulerMeanCoefficients.coefficientOrbit_iteratedFDeriv_apply {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (hA : ContDiff ℝ (↑⊤) (translateCoefficientPath A)) (n : ℕ) (a : EulerSmoothLimit.Space) (t : K) (x : EulerSmoothLimit.Space) (v : Fin n → EulerSmoothLimit.Space) : (((iteratedFDeriv ℝ n (translateCoefficientPath A) a) v) t) x = (iteratedFDeriv ℝ n (⇑(A t)) (x + a)) v

theorem EulerMeanCoefficients.coefficientOrbit_fderiv_apply {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (hA : ContDiff ℝ (↑⊤) (translateCoefficientPath A)) (a v : EulerSmoothLimit.Space) (t : K) (x : EulerSmoothLimit.Space) : (((fderiv ℝ (translateCoefficientPath A) a) v) t) x = (fderiv ℝ (⇑(A t)) (x + a)) v

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

The derivative is itself an actual continuous path of bounded fields.

Equations

• EulerMeanCoefficients.orbitDerivativePath A v = (fderiv ℝ (EulerMeanCoefficients.translateCoefficientPath A) 0) v

theorem EulerMeanCoefficients.orbitDerivativePath_apply {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (hA : ContDiff ℝ (↑⊤) (translateCoefficientPath A)) (v : EulerSmoothLimit.Space) (t : K) (x : EulerSmoothLimit.Space) : ((orbitDerivativePath A v) t) x = (fderiv ℝ (⇑(A t)) x) v

theorem EulerMeanCoefficients.orbitDerivativePath_translation {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (hA : ContDiff ℝ (↑⊤) (translateCoefficientPath A)) (v a : EulerSmoothLimit.Space) : translateCoefficientPath (orbitDerivativePath A v) a = (fderiv ℝ (translateCoefficientPath A) a) v

theorem EulerMeanCoefficients.orbitDerivativePath_orbit {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (hA : ContDiff ℝ (↑⊤) (translateCoefficientPath A)) (v : EulerSmoothLimit.Space) : ContDiff ℝ (↑⊤) (translateCoefficientPath (orbitDerivativePath A v))

theorem EulerMeanCoefficients.coefficientOrbit_norm_iteratedFDeriv_le {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (hA : ContDiff ℝ (↑⊤) (translateCoefficientPath A)) (n : ℕ) (t : K) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(A t)) x‖ ≤ ‖iteratedFDeriv ℝ n (translateCoefficientPath A) 0‖

A single genuine Banach-space derivative at zero controls the spatial derivative uniformly at every time and spatial point.