Pointwise time differentiation of actual matrix fields yields differentiation of their L² multiplication operators. The bridge is proved by evaluating the Bochner fundamental theorem of calculus, not by assuming operator derivatives.

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientTime1 : NormedAddCommGroup Field

Cache the standard NormedAddCommGroup Field instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instMeanCoefficientTime1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientTime2 : NormedSpace ℝ Field

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

Equations

• EulerMeanCoefficients.instMeanCoefficientTime2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanCoefficients.instMeanCoefficientTime3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanCoefficients.instMeanCoefficientTime4 = inferInstance

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

Operator path, given by ⟨fun t => multiplierMap (A t), multiplierMap.continuous.comp A.continuous⟩.

Equations

• EulerMeanCoefficients.operatorPath T A = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerMeanCoefficients.multiplierMap (A t), continuous_toFun := ⋯ }

theorem EulerMeanCoefficients.field_integral_eq_sub (T : ℝ) (hT : 0 ≤ T) (A A' : C(↑(Set.Icc 0 T), Field)) (hpoint : ∀ t ∈ Set.Icc 0 T, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT A s) x) ((EulerVolterraConvolution.extendPath T hT A' t) x) (Set.Icc 0 T) t) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ∫ (s : ℝ) in 0..t, EulerVolterraConvolution.extendPath T hT A' s = EulerVolterraConvolution.extendPath T hT A t - EulerVolterraConvolution.extendPath T hT A 0

theorem EulerMeanCoefficients.field_hasDerivWithinAt (T : ℝ) (hT : 0 ≤ T) (A A' : C(↑(Set.Icc 0 T), Field)) (hpoint : ∀ t ∈ Set.Icc 0 T, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT A s) x) ((EulerVolterraConvolution.extendPath T hT A' t) x) (Set.Icc 0 T) t) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (EulerVolterraConvolution.extendPath T hT A' t) (Set.Icc 0 T) t

Pointwise matrix derivatives and sup-norm continuity of the derivative are sufficient.

theorem EulerMeanCoefficients.operatorPath_hasDerivWithinAt (T : ℝ) (hT : 0 ≤ T) (A A' : C(↑(Set.Icc 0 T), Field)) (hpoint : ∀ t ∈ Set.Icc 0 T, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT A s) x) ((EulerVolterraConvolution.extendPath T hT A' t) x) (Set.Icc 0 T) t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (operatorPath T A)) ((operatorPath T A') t) (Set.Icc 0 T) ↑t

The operator-valued derivative used by the mean solver follows from the matrix-field derivative.

theorem EulerMeanCoefficients.operatorPath_inverse (T : ℝ) (A B : C(↑(Set.Icc 0 T), Field)) (hAB : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), ((A t) x) (((B t) x) v) = v) (t : ↑(Set.Icc 0 T)) (u : ↥EulerMeanSolenoidal.L2) : ((operatorPath T A) t) (((operatorPath T B) t) u) = u

theorem EulerMeanCoefficients.operatorPath_quadratic_upper (T : ℝ) (A : C(↑(Set.Icc 0 T), Field)) (K : ℝ) (hA : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((A t) x) v) v ≤ K * ‖v‖ ^ 2) (t : ↑(Set.Icc 0 T)) (u : ↥EulerMeanSolenoidal.L2) : inner ℝ (((operatorPath T A) t) u) u ≤ K * ‖u‖ ^ 2