The actual cylinder endpoint inverse agrees at every spatial/angular point with the finite-dimensional stationary history. The proof first recovers genuine coordinate representatives and their time derivatives, then uses the proved two-endpoint energy uniqueness theorem.
Actual pointwise representatives for coordinate spaces embedded in Space. A fixed bounded embedding and left inverse transfer the proved H³ point evaluation. This will apply to the two-dimensional reference plane, without identifying an L² normal with a pointwise normal vector.
noncomputable def
EulerCylinderRetractRepresentative.pointField
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[NormedSpace ℝ U]
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
{K : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P U)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(t : K)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
U
Point field, given by L (EulerCylinderSmoothOrbit.pointField P (pathMap P J p) (pathMap_orbit_contDiff P J p hp) t x).
Equations
- EulerCylinderRetractRepresentative.pointField P J L p hp t x = L (EulerCylinderSmoothOrbit.pointField P ((EulerCylinderConstantMap.pathMap P J) p) ⋯ t x)
Instances For
theorem
EulerCylinderRetractRepresentative.pointField_joint_continuous
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[NormedSpace ℝ U]
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
{K : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P U)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
:
Continuous fun (z : K × EulerLiftedGradientSpace.LiftDomain P) => pointField P J L p hp z.1 z.2
theorem
EulerCylinderRetractRepresentative.pointField_smooth
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[NormedSpace ℝ U]
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
{K : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P U)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(t : K)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (pointField P J L p hp t) x)
theorem
EulerCylinderRetractRepresentative.pointField_continuous
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[NormedSpace ℝ U]
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
{K : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P U)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(t : K)
:
Continuous (pointField P J L p hp t)
noncomputable def
EulerCylinderRetractRepresentative.pointPath
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[NormedSpace ℝ U]
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
{K : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P U)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
Point path as an element of C(K,U).
Equations
- EulerCylinderRetractRepresentative.pointPath P J L p hp x = { toFun := fun (t : K) => EulerCylinderRetractRepresentative.pointField P J L p hp t x, continuous_toFun := ⋯ }
Instances For
theorem
EulerCylinderRetractRepresentative.pointField_ae
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[NormedSpace ℝ U]
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
{K : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P U)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(hL : ∀ (v : U), L (J v) = v)
(t : K)
:
↑↑(p t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] pointField P J L p hp t
theorem
EulerCylinderRetractRepresentative.pointField_eq
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[NormedSpace ℝ U]
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
{K : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P U)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(hL : ∀ (v : U), L (J v) = v)
(t : K)
(f : EulerLiftedGradientSpace.LiftDomain P → U)
(hf : Continuous f)
(hrep : ↑↑(p t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f)
:
theorem
EulerCylinderRetractRepresentative.pointPath_hasDerivWithinAt
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[NormedSpace ℝ U]
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(T : ℝ)
(hT : 0 ≤ T)
(p q : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t)
(x : EulerLiftedGradientSpace.LiftDomain P)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (pointPath P J L p hp x)) ((pointPath P J L q hq x) t)
(Set.Icc 0 T) ↑t
Initial time integration commutes with the genuine mixed cylinder action.
theorem
EulerCylinderPathIntegral.integral_translate
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[CompleteSpace V]
(T : ℝ)
(hT : 0 ≤ T)
(p : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P V)))
(a : EulerLiftedGradientSpace.LiftTangent)
:
theorem
EulerCylinderPathIntegral.integral_orbit_contDiff
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[CompleteSpace V]
(T : ℝ)
(hT : 0 ≤ T)
(p : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P V)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeIntegral.integral T hT) p)
theorem
EulerCylinderPathIntegral.orbit_contDiff_of_derivative
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[CompleteSpace V]
(T : ℝ)
(hT : 0 ≤ T)
(p q : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P V)))
(hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t)
(hzero : p ⟨0, ⋯⟩ = 0)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p
theorem
EulerCylinderDirichlet.Coefficients.endpointDisplacement_orbit_contDiff
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) ((endpointDisplacement P D) Y)
noncomputable def
EulerCylinderDirichlet.Coefficients.endpointPointDisplacement
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
Endpoint point displacement, given by pointPath P J L (D.endpointDisplacement P Y) (D.endpointDisplacement_orbit_contDiff P hQ hQ₁ hH Y hY) x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerCylinderDirichlet.Coefficients.endpointPointCoordinate
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
Endpoint point coordinate, given by pointPath P J L (D.endpointCoordinate P Y) (D.endpointCoordinate_orbit_contDiff P hQ hQ₁ hH Y hY) x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerCylinderDirichlet.Coefficients.endpointPointAcceleration
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
Endpoint point acceleration, given by pointPath P J L (D.endpointAcceleration P Y) (D.endpointAcceleration_orbit_contDiff P hQ hQ₁ hH Y hY) x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCylinderDirichlet.Coefficients.endpointPointDisplacement_hasDerivWithinAt
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(x : EulerLiftedGradientSpace.LiftDomain P)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ (endpointPointDisplacement P D J L hQ hQ₁ hH Y hY x))
((endpointPointCoordinate P D J L hQ hQ₁ hH Y hY x) t) (Set.Icc 0 T) ↑t
theorem
EulerCylinderDirichlet.Coefficients.endpointPointCoordinate_hasDerivWithinAt
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(x : EulerLiftedGradientSpace.LiftDomain P)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ (endpointPointCoordinate P D J L hQ hQ₁ hH Y hY x))
((endpointPointAcceleration P D J L hQ hQ₁ hH Y hY x) t) (Set.Icc 0 T) ↑t
theorem
EulerCylinderDirichlet.Coefficients.endpointPointCoordinate_ae
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(hL : ∀ (v : U), L (J v) = v)
(t : ↑(Set.Icc 0 T))
:
↑↑(((endpointCoordinate P D) Y) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) => (endpointPointCoordinate P D J L hQ hQ₁ hH Y hY x) t
theorem
EulerCylinderDirichlet.Coefficients.endpointPointAcceleration_ae
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(hL : ∀ (v : U), L (J v) = v)
(t : ↑(Set.Icc 0 T))
:
↑↑(((endpointAcceleration P D) Y) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) => (endpointPointAcceleration P D J L hQ hQ₁ hH Y hY x) t
theorem
EulerCylinderDirichlet.Coefficients.endpointPointDisplacement_initial
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(hL : ∀ (v : U), L (J v) = v)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
theorem
EulerCylinderDirichlet.Coefficients.endpointPointDisplacement_terminal
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(hL : ∀ (v : U), L (J v) = v)
(f : EulerLiftedGradientSpace.LiftDomain P → U)
(hf : Continuous f)
(hrep : ↑↑Y =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
theorem
EulerCylinderDirichlet.Coefficients.endpointPoint_projected_equation
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(hL : ∀ (v : U), L (J v) = v)
(x : EulerLiftedGradientSpace.LiftDomain P)
(t : ↑(Set.Icc 0 T))
:
(EulerTransverseGramInverse.gram ((D.Q t) x.1)) ((endpointPointAcceleration P D J L hQ hQ₁ hH Y hY x) t) = (ContinuousLinearMap.adjoint ((D.Q t) x.1))
(-2 • ((D.Q₁ t) x.1) ((endpointPointCoordinate P D J L hQ hQ₁ hH Y hY x) t))
theorem
EulerCylinderDirichlet.Coefficients.endpointPointCoordinate_eq_label
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(hL : ∀ (v : U), L (J v) = v)
(f : EulerLiftedGradientSpace.LiftDomain P → U)
(hf : Continuous f)
(hrep : ↑↑Y =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
theorem
EulerCylinderDirichlet.Coefficients.endpointVelocity_pointwise
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Coefficients T U EulerSmoothLimit.Space)
(J : U →L[ℝ] EulerSmoothLimit.Space)
(L : EulerSmoothLimit.Space →L[ℝ] U)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) Y)
(hL : ∀ (v : U), L (J v) = v)
(f : EulerLiftedGradientSpace.LiftDomain P → U)
(hf : Continuous f)
(hrep : ↑↑Y =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f)
(x : EulerLiftedGradientSpace.LiftDomain P)
(t : ↑(Set.Icc 0 T))
:
EulerCylinderSmoothOrbit.pointField P ((endpointVelocity P D) Y) ⋯ t x = ((D.labelVelocity x.1) (f x)) t