Evaluation of the actual cylinder coefficients at a spatial label.

noncomputable def EulerCylinderDirichlet.Coefficients.labelFrame {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (x : EulerSmoothLimit.Space) : C(↑(Set.Icc 0 T), U →L[ℝ] E)

Label frame, given by pathEvaluation x D.Q.

Equations

• D.labelFrame x = (EulerTransverseSourceCoefficientPath.pathEvaluation x) D.Q

noncomputable def EulerCylinderDirichlet.Coefficients.labelFrameDerivative {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (x : EulerSmoothLimit.Space) : C(↑(Set.Icc 0 T), U →L[ℝ] E)

Label frame derivative, given by pathEvaluation x D.Q₁.

Equations

• D.labelFrameDerivative x = (EulerTransverseSourceCoefficientPath.pathEvaluation x) D.Q₁

noncomputable def EulerCylinderDirichlet.Coefficients.labelFrameSecond {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (x : EulerSmoothLimit.Space) : C(↑(Set.Icc 0 T), U →L[ℝ] E)

Label frame second, given by pathEvaluation x D.Q₂.

Equations

• D.labelFrameSecond x = (EulerTransverseSourceCoefficientPath.pathEvaluation x) D.Q₂

noncomputable def EulerCylinderDirichlet.Coefficients.labelHessian {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (x : EulerSmoothLimit.Space) : C(↑(Set.Icc 0 T), E →L[ℝ] E)

Label hessian, given by pathEvaluation x D.H.

Equations

• D.labelHessian x = (EulerTransverseSourceCoefficientPath.pathEvaluation x) D.H

theorem EulerCylinderDirichlet.Coefficients.labelFrame_lower {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (x : EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 T)) (v : U) : D.lower * ‖v‖ ^ 2 ≤ ‖((D.labelFrame x) t) v‖ ^ 2

theorem EulerCylinderDirichlet.Coefficients.labelFrame_derivative {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (x : EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ (D.labelFrame x)) ((D.labelFrameDerivative x) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderDirichlet.Coefficients.labelFrame_second_derivative {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (x : EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ (D.labelFrameDerivative x)) ((D.labelFrameSecond x) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderDirichlet.Coefficients.labelFrame_equation {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (x : EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 T)) : (D.labelFrameSecond x) t = -(D.labelHessian x) t ∘SL (D.labelFrame x) t

theorem EulerCylinderDirichlet.Coefficients.labelHessian_upper {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (x : EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 T)) (v : E) : inner ℝ (((D.labelHessian x) t) v) v ≤ D.potential * ‖v‖ ^ 2

noncomputable def EulerCylinderDirichlet.Coefficients.labelCoordinate {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) (x : EulerSmoothLimit.Space) : U →L[ℝ] C(↑(Set.Icc 0 T), U)

The already constructed finite-dimensional stationary history, at this label, applied to an ordinary terminal coordinate.

Equations

• D.labelCoordinate x = EulerTransverseEndpointCoordinates.continuousCoordinateVelocity T ⋯ (D.labelFrame x) (D.labelFrameDerivative x) (D.labelHessian x) D.lower ⋯ ⋯ ⋯ D.potential ⋯ ⋯ ⋯

noncomputable def EulerCylinderDirichlet.Coefficients.labelVelocity {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) (x : EulerSmoothLimit.Space) : U →L[ℝ] C(↑(Set.Icc 0 T), E)

Label velocity, constructed using historyVelocity.

Equations

• D.labelVelocity x = EulerTransverseEndpointCoordinates.historyVelocity T ⋯ (D.labelFrame x) (D.labelFrameDerivative x) (D.labelHessian x) D.lower ⋯ ⋯ ⋯ D.potential ⋯ ⋯ ⋯

theorem EulerCylinderDirichlet.Coefficients.labelVelocity_apply {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) (x : EulerSmoothLimit.Space) (Y : U) (t : ↑(Set.Icc 0 T)) : ((D.labelVelocity x) Y) t = ((D.Q t) x) (((D.labelCoordinate x) Y) t)