Commuting actual spatial derivatives with the time derivative

The time integral is a fixed bounded linear map on continuous L² paths. Differentiating its exact identity in the translation parameter therefore commutes every spatial jet with the time integral. The resulting finite Sobolev arrays transfer the actual time derivative to the smooth spatial representatives.

@[instance_reducible]

noncomputable def EulerMeanPathTimeDerivative.instMeanPathTimeDerivative1 : NormedAddCommGroup ↥EulerMeanSolenoidal.L2

Cache the standard NormedAddCommGroup L2 instance to shorten typeclass synthesis.

Equations

• EulerMeanPathTimeDerivative.instMeanPathTimeDerivative1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPathTimeDerivative.instMeanPathTimeDerivative2 : NormedSpace ℝ ↥EulerMeanSolenoidal.L2

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

Equations

• EulerMeanPathTimeDerivative.instMeanPathTimeDerivative2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPathTimeDerivative.instMeanPathTimeDerivative3 : AddCommGroup ↥EulerMeanSolenoidal.L2

Cache the standard AddCommGroup L2 instance to shorten typeclass synthesis.

Equations

• EulerMeanPathTimeDerivative.instMeanPathTimeDerivative3 = inferInstance.toAddCommGroup

@[instance_reducible]

noncomputable def EulerMeanPathTimeDerivative.instMeanPathTimeDerivative4 : Module ℝ ↥EulerMeanSolenoidal.L2

Cache the standard Module ℝ L2 instance to shorten typeclass synthesis.

Equations

• EulerMeanPathTimeDerivative.instMeanPathTimeDerivative4 = inferInstance.toModule

@[instance_reducible]

noncomputable def EulerMeanPathTimeDerivative.instMeanPathTimeDerivative5 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanPathTimeDerivative.instMeanPathTimeDerivative5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPathTimeDerivative.instMeanPathTimeDerivative6 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanPathTimeDerivative.instMeanPathTimeDerivative6 T = inferInstance

noncomputable def EulerMeanPathTimeDerivative.initialValueMap (T : ℝ) (hT : 0 ≤ T) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2) →L[ℝ] C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

The constant path with the same initial value, as an actual bounded linear map.

Equations

• EulerMeanPathTimeDerivative.initialValueMap T hT = ContinuousLinearMap.const ℝ ↑(Set.Icc 0 T) ∘SL ContinuousMap.evalCLM ℝ ⟨0, ⋯⟩

theorem EulerMeanPathTimeDerivative.path_integral_identity (T : ℝ) (hT : 0 ≤ T) (p q : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hder : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t) (a : EulerSmoothLimit.Space) : (EulerMeanTimeContinuousTranslation.pathTranslation T a) p = (initialValueMap T hT) ((EulerMeanTimeContinuousTranslation.pathTranslation T a) p) + (EulerContinuousTimeIntegral.integral T hT) ((EulerMeanTimeContinuousTranslation.pathTranslation T a) q)

The exact time-integral identity holds after every actual spatial translation.

theorem EulerMeanPathTimeDerivative.spatialJetPath_integral_identity (T : ℝ) (hT : 0 ≤ T) (p q : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hder : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) q) (n : ℕ) (v : Fin n → EulerSmoothLimit.Space) : (iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) 0) v = (initialValueMap T hT) ((iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) 0) v) + (EulerContinuousTimeIntegral.integral T hT) ((iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) q) 0) v)

Every genuine spatial jet satisfies the same exact bounded time-integral identity.

theorem EulerMeanPathTimeDerivative.spatialJetPath_hasDerivWithinAt (T : ℝ) (hT : 0 ≤ T) (p q : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hder : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) q) (n : ℕ) (v : Fin n → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT ((iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) 0) v)) (((iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) q) 0) v) t) (Set.Icc 0 T) ↑t

Every actual spatial jet has the time derivative obtained by differentiating q.

theorem EulerMeanPathTimeDerivative.instMeanPathTimeDerivative7 : Fact (0 < 1)

theorem EulerMeanPathTimeDerivative.ordinarySobolev_hasDerivWithinAt (T : ℝ) (hT : 0 ≤ T) (p q : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hder : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) q) (k : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (fun (r : ℝ) => EulerMeanSmoothRepresentative.ordinarySobolev k (EulerVolterraConvolution.extendPath T hT p r) ⋯) (EulerMeanSmoothRepresentative.ordinarySobolev k (q t) ⋯) (Set.Icc 0 T) ↑t

The complete finite Sobolev array has the actual time derivative; no separate mixed-jet assumption is needed.

theorem EulerMeanPathTimeDerivative.representative_hasDerivWithinAt (T : ℝ) (hT : 0 ≤ T) (p q : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hder : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) q) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (r : ℝ) => EulerMeanSmoothRepresentative.representative (EulerVolterraConvolution.extendPath T hT p r) ⋯ x) (EulerMeanSmoothRepresentative.representative (q t) ⋯ x) (Set.Icc 0 T) ↑t

The smooth ordinary-space representative has the actual classical time derivative represented by q, including within-interval endpoint derivatives.