All-order parameter regularity of actual bounded smooth coefficient translations.

theorem EulerMeanCoefficients.fieldDerivativeMap_norm_le {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V)) : ‖fieldDerivativeMap DA‖ ≤ ‖DA‖

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

Derivative bundling linear, bundling toFun, map_add, map_smul.

Equations

• EulerMeanCoefficients.derivativeBundlingLinear = { toFun := EulerMeanCoefficients.fieldDerivativeMap, map_add' := ⋯, map_smul' := ⋯ }

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

Currying a bounded field of linear maps is itself a bounded linear operation.

Equations

• EulerMeanCoefficients.derivativeBundling = { toLinearMap := EulerMeanCoefficients.derivativeBundlingLinear, cont := ⋯ }

@[simp]

theorem EulerMeanCoefficients.derivativeBundling_apply {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V)) : derivativeBundling A = fieldDerivativeMap A

structure EulerMeanCoefficients.BoundedSmoothField (V : Type u) [NormedAddCommGroup V] [NormedSpace ℝ V] : Type u

A concrete smooth coefficient with globally bounded actual derivatives of every order.

• field : BoundedContinuousFunction EulerSmoothLimit.Space V

  Underlying field of BoundedSmoothField, of type Space →ᵇ V.

• smooth : ContDiff ℝ ↑⊤ ⇑self.field
• bounded (n : ℕ) : ∃ (C : ℝ), ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑self.field) x‖ ≤ C

noncomputable def EulerMeanCoefficients.BoundedSmoothField.derivative {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : BoundedSmoothField V) : BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] V)

Derivative, bundling field, smooth, bounded.

Equations

• A.derivative = { field := EulerMeanCoefficients.boundedDerivative A.field ⋯ (Classical.choose ⋯) ⋯, smooth := ⋯, bounded := ⋯ }

@[simp]

theorem EulerMeanCoefficients.BoundedSmoothField.derivative_field_apply {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : BoundedSmoothField V) (x : EulerSmoothLimit.Space) : A.derivative.field x = fderiv ℝ (⇑A.field) x

theorem EulerMeanCoefficients.BoundedSmoothField.translation_hasFDerivAt {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : BoundedSmoothField V) (a : EulerSmoothLimit.Space) : HasFDerivAt (translated A.field) (fieldDerivativeMap (translated A.derivative.field a)) a

theorem EulerMeanCoefficients.BoundedSmoothField.translation_fderiv {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : BoundedSmoothField V) : fderiv ℝ (translated A.field) = fun (a : EulerSmoothLimit.Space) => derivativeBundling (translated A.derivative.field a)

theorem EulerMeanCoefficients.BoundedSmoothField.translation_contDiff {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : BoundedSmoothField V) : ContDiff ℝ (↑⊤) (translated A.field)

Every spatial translation of an actual globally bounded smooth coefficient depends smoothly on its parameter.