Uniform time-path bounds for actual spatial derivatives of the multiplication operators.

@[instance_reducible]

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

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

Equations

• EulerMeanCoefficients.instMeanCoefficientPathJets1 = inferInstance

@[instance_reducible]

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

theorem EulerMeanCoefficients.SmoothCoefficientPath.iteratedFDeriv_translation_apply {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (n : ℕ) (a : EulerSmoothLimit.Space) (t : K) (x : EulerSmoothLimit.Space) (v : Fin n → EulerSmoothLimit.Space) : (((iteratedFDeriv ℝ n (translateCoefficientPath A.field) a) v) t) x = (iteratedFDeriv ℝ n (⇑(A.field t)) (x + a)) v

theorem EulerMeanCoefficients.SmoothCoefficientPath.norm_iteratedFDeriv_translation_le {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath K V) (n : ℕ) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(A.field t)) x‖ ≤ C) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (translateCoefficientPath A.field) a‖ ≤ C

A pointwise coefficient-derivative bound is a bound in the actual uniform path norm.

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientPathJets3 : NormedAddCommGroup Field

Cache the standard NormedAddCommGroup Field instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instMeanCoefficientPathJets3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientPathJets4 : NormedSpace ℝ Field

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

Equations

• EulerMeanCoefficients.instMeanCoefficientPathJets4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientPathJets5 : NormedAddCommGroup (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanCoefficients.instMeanCoefficientPathJets5 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientPathJets6 : NormedSpace ℝ (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanCoefficients.instMeanCoefficientPathJets6 = inferInstance

noncomputable def EulerMeanCoefficients.operatorPathMap (T : ℝ) : C(↑(Set.Icc 0 T), Field) →L[ℝ] C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Operator path map, given by multiplierMap.compLeftContinuous ℝ (Icc (0 : ℝ) T).

Equations

• EulerMeanCoefficients.operatorPathMap T = ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) EulerMeanCoefficients.multiplierMap

@[simp]

theorem EulerMeanCoefficients.operatorPathMap_apply (T : ℝ) (A : C(↑(Set.Icc 0 T), Field)) : (operatorPathMap T) A = operatorPath T A

theorem EulerMeanCoefficients.operatorPathMap_norm_le_one (T : ℝ) : ‖operatorPathMap T‖ ≤ 1

theorem EulerMeanCoefficients.operatorPathTranslation_contDiff (T : ℝ) (A : SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => operatorPath T (translatedPath T A.field a)

theorem EulerMeanCoefficients.norm_iteratedFDeriv_operatorPathTranslation_le (T : ℝ) (A : SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (n : ℕ) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(A.field t)) x‖ ≤ C) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => operatorPath T (translatedPath T A.field b)) a‖ ≤ C

The true parameter derivatives of the operator path inherit the exact pointwise bounds.