Spatial translations and their genuine uniform-norm derivatives for matrix coefficients.

def EulerMeanCoefficients.translated {V : Type u_1} [NormedAddCommGroup V] (A : BoundedContinuousFunction EulerSmoothLimit.Space V) (a : EulerSmoothLimit.Space) : BoundedContinuousFunction EulerSmoothLimit.Space V

Translated, given by A.compContinuous ⟨fun x => x+a, continuous_id.add continuous_const⟩.

Equations

• EulerMeanCoefficients.translated A a = A.compContinuous { toFun := fun (x : EulerSmoothLimit.Space) => x + a, continuous_toFun := ⋯ }

@[simp]

theorem EulerMeanCoefficients.translated_apply {V : Type u_1} [NormedAddCommGroup V] (A : BoundedContinuousFunction EulerSmoothLimit.Space V) (a x : EulerSmoothLimit.Space) : (translated A a) x = A (x + a)

@[simp]

theorem EulerMeanCoefficients.translated_zero {V : Type u_1} [NormedAddCommGroup V] (A : BoundedContinuousFunction EulerSmoothLimit.Space V) : translated A 0 = A

theorem EulerMeanCoefficients.translated_add {V : Type u_1} [NormedAddCommGroup V] (A : BoundedContinuousFunction EulerSmoothLimit.Space V) (a b : EulerSmoothLimit.Space) : translated (translated A a) b = translated A (b + a)

theorem EulerMeanCoefficients.translated_norm_le {V : Type u_1} [NormedAddCommGroup V] (A : BoundedContinuousFunction EulerSmoothLimit.Space V) (a : EulerSmoothLimit.Space) : ‖translated A a‖ ≤ ‖A‖

noncomputable def EulerMeanCoefficients.boundedDerivative {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : BoundedContinuousFunction EulerSmoothLimit.Space V) (hA : ContDiff ℝ ↑⊤ ⇑A) (C : ℝ) (hC : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (⇑A) x‖ ≤ C) : BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V)

Bounded derivative, given by BoundedContinuousFunction.ofNormedAddCommGroup (fderiv ℝ (A : Space → V)) (hA.fderiv_right (m := ∞) (by simp)).continuous C hC.

Equations

• EulerMeanCoefficients.boundedDerivative A hA C hC = BoundedContinuousFunction.ofNormedAddCommGroup (fderiv ℝ ⇑A) ⋯ C hC

noncomputable def EulerMeanCoefficients.fieldDirection {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V)) (a : EulerSmoothLimit.Space) : BoundedContinuousFunction EulerSmoothLimit.Space V

Field direction, constructed using BoundedContinuousFunction.ofNormedAddCommGroup.

Equations

• EulerMeanCoefficients.fieldDirection DA a = BoundedContinuousFunction.ofNormedAddCommGroup (fun (x : EulerSmoothLimit.Space) => (DA x) a) ⋯ (‖DA‖ * ‖a‖) ⋯

@[simp]

theorem EulerMeanCoefficients.fieldDirection_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V)) (a x : EulerSmoothLimit.Space) : (fieldDirection DA a) x = (DA x) a

theorem EulerMeanCoefficients.fieldDirection_norm_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V)) (a : EulerSmoothLimit.Space) : ‖fieldDirection DA a‖ ≤ ‖DA‖ * ‖a‖

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

Field derivative linear, bundling toFun, map_add, map_smul.

Equations

• EulerMeanCoefficients.fieldDerivativeLinear DA = { toFun := EulerMeanCoefficients.fieldDirection DA, map_add' := ⋯, map_smul' := ⋯ }

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

Field derivative map, bundling toLinearMap, cont.

Equations

• EulerMeanCoefficients.fieldDerivativeMap DA = { toLinearMap := EulerMeanCoefficients.fieldDerivativeLinear DA, cont := ⋯ }

@[simp]

theorem EulerMeanCoefficients.fieldDerivativeMap_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (DA : BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V)) (a x : EulerSmoothLimit.Space) : ((fieldDerivativeMap DA) a) x = (DA x) a

theorem EulerMeanCoefficients.translated_taylor_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : BoundedContinuousFunction EulerSmoothLimit.Space V) (DA : BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V)) (hA : ContDiff ℝ ↑⊤ ⇑A) (hDA : ∀ (x : EulerSmoothLimit.Space), DA x = fderiv ℝ (⇑A) x) (M : ℝ) (hM : 0 ≤ M) (h₂ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ ⇑A) x‖ ≤ M) (a b : EulerSmoothLimit.Space) : ‖translated A b - translated A a - (fieldDerivativeMap (translated DA a)) (b - a)‖ ≤ M * ‖b - a‖ ^ 2

theorem EulerMeanCoefficients.translated_hasFDerivAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : BoundedContinuousFunction EulerSmoothLimit.Space V) (DA : BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V)) (hA : ContDiff ℝ ↑⊤ ⇑A) (hDA : ∀ (x : EulerSmoothLimit.Space), DA x = fderiv ℝ (⇑A) x) (M : ℝ) (hM : 0 ≤ M) (h₂ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ ⇑A) x‖ ≤ M) (a : EulerSmoothLimit.Space) : HasFDerivAt (translated A) (fieldDerivativeMap (translated DA a)) a

Bounded actual second derivatives yield the true Fréchet derivative of translation in sup norm.

theorem EulerMeanCoefficients.multiplier_translation (A : Field) (a : EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) : (EulerMeanSolenoidal.translation a) ((multiplier A) u) = (multiplier (translated A a)) ((EulerMeanSolenoidal.translation a) u)

Multiplication by an actual translated coefficient intertwines the ordinary L² translations.