The literal homogeneous physical equation for the constructed nonzero - terminal cylinder history. Pointwise tangency and the normal residual are deduced from the actual frame range; there is no single L² normal vector.
theorem
EulerCylinderDirichlet.Coefficients.endpoint_coordinate_equation_ae
(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)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(t : ↑(Set.Icc 0 T))
:
∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain P) ∂EulerLiftedGradientSpace.liftMeasure P, (EulerTransverseGramInverse.gram ((D.Q t) x.1)) (↑↑(((endpointAcceleration P D) Y) t) x) = (ContinuousLinearMap.adjoint ((D.Q t) x.1)) (-2 • ((D.Q₁ t) x.1) (↑↑(((endpointCoordinate P D) Y) t) x))
theorem
EulerCylinderDirichlet.Coefficients.endpointVelocity_ae
(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)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(t : ↑(Set.Icc 0 T))
:
↑↑(((endpointVelocity P D) Y) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P]
fun (x : EulerLiftedGradientSpace.LiftDomain P) => ((D.Q t) x.1) (↑↑(((endpointCoordinate P D) Y) t) x)
theorem
EulerCylinderDirichlet.Coefficients.endpointDerivative_ae
(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)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(t : ↑(Set.Icc 0 T))
:
↑↑(((endpointDerivative P D) Y) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P]
fun (x : EulerLiftedGradientSpace.LiftDomain P) =>
((D.Q₁ t) x.1) (↑↑(((endpointCoordinate P D) Y) t) x) + ((D.Q t) x.1) (↑↑(((endpointAcceleration P D) Y) t) x)
theorem
EulerCylinderDirichlet.Coefficients.endpoint_physical_balance_ae
(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)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(M : ↑(Set.Icc 0 T) → EulerSmoothLimit.Space → E →L[ℝ] E)
(m : ↑(Set.Icc 0 T) → EulerSmoothLimit.Space → E)
(hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), m t x ≠ 0)
(hTangent : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), inner ℝ (m t x) (((D.Q t) x) v) = 0)
(hRange :
∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (η : E), inner ℝ (m t x) η = 0 → ∃ (v : U), ((D.Q t) x) v = η)
(hFlow : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.Q₁ t) x = M t x ∘SL (D.Q t) x)
(t : ↑(Set.Icc 0 T))
:
∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain P) ∂EulerLiftedGradientSpace.liftMeasure P, ↑↑(((endpointDerivative P D) Y) t) x + (M t x.1) (↑↑(((endpointVelocity P D) Y) t) x) + (-(2 * inner ℝ (m t x.1) ((M t x.1) (↑↑(((endpointVelocity P D) Y) t) x))) / ‖m t x.1‖ ^ 2) • m t x.1 = 0