Actual mixed-translation smoothness of the cylinder history

The translated variational problems live on one fixed Hilbert space. Smoothness follows from their genuine coercive inverses, and exact covariance identifies that family with the translation orbit of the constructed field. No regularity assumption is imposed on a solved history field.

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity1 (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 P U)

Cache the standard NormedAddCommGroup (CylinderL2 P U) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity1 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity2 (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 P U)

Cache the standard NormedSpace ℝ (CylinderL2 P U) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity3 (P : ℝ) [Fact (0 < P)] {E : Type u_2} [NormedAddCommGroup E] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 P E)

Cache the standard NormedAddCommGroup (CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity3 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity4 (P : ℝ) [Fact (0 < P)] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 P E)

Cache the standard NormedSpace ℝ (CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity4 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity5 (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Cache the standard NormedAddCommGroup (CylinderL2 P U →L[ℝ] CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity5 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity6 (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Cache the standard NormedSpace ℝ (CylinderL2 P U →L[ℝ] CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity6 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity7 (P : ℝ) [Fact (0 < P)] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

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

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity7 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity8 (P : ℝ) [Fact (0 < P)] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

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

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity8 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity9 (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,CylinderL2 P U →L[ℝ] CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity9 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity10 (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,CylinderL2 P U →L[ℝ] CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity10 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity11 (P : ℝ) [Fact (0 < P)] {T : ℝ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,CylinderL2 P E →L[ℝ] CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity11 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity12 (P : ℝ) [Fact (0 < P)] {T : ℝ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,CylinderL2 P E →L[ℝ] CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletRegularity12 P = inferInstance

theorem EulerCylinderDirichlet.Coefficients.frameOrbit_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)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => frame P (D.shifted a.1)

theorem EulerCylinderDirichlet.Coefficients.frameDerivativeOrbit_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₁)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => frameDerivative P (D.shifted a.1)

theorem EulerCylinderDirichlet.Coefficients.hessianOrbit_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) (hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => hessian P (D.shifted a.1)

theorem EulerCylinderDirichlet.Coefficients.accelerationLp_translation (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) (a : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E))) : (accelerationLp P (D.shifted a.1)) ((EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) f) = (EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) ((accelerationLp P D) f)

theorem EulerCylinderDirichlet.Coefficients.velocityLp_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)) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) f) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) ((velocityLp P D) f)

theorem EulerCylinderDirichlet.Coefficients.accelerationLp_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)) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) f) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) ((accelerationLp P D) f)

theorem EulerCylinderDirichlet.Coefficients.velocityPath_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)) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f))

theorem EulerCylinderDirichlet.Coefficients.accelerationPath_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)) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (accelerationPath P D f)

theorem EulerCylinderDirichlet.Coefficients.physicalVelocity_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)) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (physicalVelocity P D f)

theorem EulerCylinderDirichlet.Coefficients.physicalDerivative_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)) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (physicalDerivative P D f)