Time regularity of the full genuine covering derivative, reconstructed from its four directions.

noncomputable def EulerCylinderSmoothOrbit.tangentCoordinate (i : Fin 4) : EulerLiftedGradientSpace.LiftTangent →L[ℝ] ℝ

Tangent coordinate, given by (EuclideanSpace.proj i).comp coordinateEquiv.symm.toContinuousLinearMap.

Equations

• EulerCylinderSmoothOrbit.tangentCoordinate i = EuclideanSpace.proj i ∘SL ↑EulerCylinderCoordinates.coordinateEquiv.symm

noncomputable def EulerCylinderSmoothOrbit.fromCoordinates : (Fin 4 → EulerSmoothLimit.Space) →L[ℝ] EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space

From coordinates, given by ∑ i : Fin 4, (ContinuousLinearMap.smulRightL ℝ LiftTangent Space (tangentCoordinate i)).comp (ContinuousLinearMap.proj i).

Equations

• One or more equations did not get rendered due to their size.

theorem EulerCylinderSmoothOrbit.fromCoordinates_apply (u : Fin 4 → EulerSmoothLimit.Space) (v : EulerLiftedGradientSpace.LiftTangent) : (fromCoordinates u) v = ∑ i : Fin 4, (EulerCylinderCoordinates.coordinateEquiv.symm v).ofLp i • u i

theorem EulerCylinderSmoothOrbit.tangent_sum_coordinates (v : EulerLiftedGradientSpace.LiftTangent) : ∑ i : Fin 4, (EulerCylinderCoordinates.coordinateEquiv.symm v).ofLp i • EulerCylinderSobolev.standardDirection i = v

theorem EulerCylinderSmoothOrbit.fromCoordinates_eq (D : EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space) : (fromCoordinates fun (i : Fin 4) => D (EulerCylinderSobolev.standardDirection i)) = D

theorem EulerCylinderSmoothOrbit.pointField_fderiv_joint_continuous (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : Continuous fun (z : K × EulerLiftedGradientSpace.LiftDomain P) => EulerLiftedWeakDerivative.fieldFDeriv P (pointField P p hp z.1) z.2

theorem EulerCylinderSmoothOrbit.pointField_fderiv_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] (T : ℝ) (hT : 0 ≤ T) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (f t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : HasDerivWithinAt (fun (r : ℝ) => EulerLiftedWeakDerivative.fieldFDeriv P (pointField P p hp (Set.projIcc 0 T hT r)) x) (EulerLiftedWeakDerivative.fieldFDeriv P (pointField P f hf t) x) (Set.Icc 0 T) ↑t

Differentiating the full covering derivative in time gives the covering derivative of the true RHS.