Genuine mixed spatial/angular regularity of the nonzero-terminal cylinder inverse. The terminal datum's actual translation orbit is the only field regularity assumption; output regularity follows from the forced inverse.
theorem
EulerLpCylinderTranslation.constantPath_orbit_contDiff
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
{V : Type u_2}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(Y : ↥(CylinderL2 P V))
(hY : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (translate P a) Y)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) (ContinuousMap.const K Y)
theorem
EulerCylinderDirichlet.Coefficients.endpointConstant_orbit_contDiff
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(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) (ContinuousMap.const (↑(Set.Icc 0 T)) (T⁻¹ • Y))
theorem
EulerCylinderDirichlet.Coefficients.endpointForcing_orbit_contDiff
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
(D : Coefficients T U E)
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(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) ((endpointForcing P D) Y)
theorem
EulerCylinderDirichlet.Coefficients.endpointCoordinate_orbit_contDiff
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(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) ((endpointCoordinate P D) Y)
theorem
EulerCylinderDirichlet.Coefficients.endpointAcceleration_orbit_contDiff
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(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) ((endpointAcceleration P D) Y)
theorem
EulerCylinderDirichlet.Coefficients.endpointVelocity_orbit_contDiff
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(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) ((endpointVelocity P D) Y)
theorem
EulerCylinderDirichlet.Coefficients.endpointDerivative_orbit_contDiff
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(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) ((endpointDerivative P D) Y)