The actual affine-terminal fixed-coordinate variational solution satisfies the source homogeneous coordinate equation. The range condition follows from its explicit coordinate primitive. No ambient normal, nor a supplied weak equation or smooth representative, is an input to these results.
theorem
EulerFixedEndpointStrong.fixedEndpointDerivative_weak
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
(Y : V)
(v : ↥(EulerTimeLp.TimeLp T U))
(hv : (EulerTerminalTimePrimitive.initialTrace T hT) v = 0)
:
have u := (EulerTransverseFixedEndpoint.fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall L) Y;
inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) v = -inner ℝ ((EulerTransverseEndpointMomentum.initialMomentumForcing T hT Q Q₁ H) u)
((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)
The constructed fixed-coordinate endpoint inverse obeys the literal weak momentum identity, for every trial lift.
theorem
EulerFixedEndpointStrong.coordinateSlope_range
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(ξ : U)
(t : ↑(Set.Icc 0 T))
:
∃ (x : U),
(Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T
((EulerTransverseFixedEndpoint.fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall
(EulerTransverseEndpointParameter.affineTrial T hT Q Q₁))
ξ)
↑t
The affine fixed-coordinate solution lies in the actual frame range at every time, including the two endpoints.
theorem
EulerFixedEndpointStrong.coordinateSlope_ae
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(hTpos : 0 < T)
(ξ : U)
:
↑↑((EulerTransverseEndpointCoordinates.coordinateSlope T hT Q Q₁ H c hc hQ hd K hK hH hsmall)
ξ) =ᵐ[EulerTimeLp.timeMeasure T] EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H
((EulerTransverseFixedEndpoint.fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall
(EulerTransverseEndpointParameter.affineTrial T hT Q Q₁))
ξ)
The continuous momentum reconstruction represents the explicit coordinate derivative of the fixed affine-terminal solution.
theorem
EulerFixedEndpointStrong.coordinate_equation
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hTpos : 0 < T)
(hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t)
(hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t)
(ξ : U)
(t : ↑(Set.Icc 0 T))
:
have u :=
(EulerTransverseFixedEndpoint.fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall
(EulerTransverseEndpointParameter.affineTrial T hT Q Q₁))
ξ;
HasDerivWithinAt (EulerTransverseInitialCoordinates.initialCoordinates T hT Q c hc hQ u)
(EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H u ↑t) (Set.Icc 0 T) ↑t ∧ HasDerivWithinAt (EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H u)
(((EulerTransverseForwardInverse.generator T Q Q₁ c hc hQ) t)
(EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H u ↑t))
(Set.Icc 0 T) ↑t
Equation (10) for the constructed affine-terminal fixed-space inverse.
theorem
EulerFixedEndpointStrong.coordinateSlope_h1
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hTpos : 0 < T)
(hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t)
(hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t)
(ξ : U)
:
have v :=
EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H
((EulerTransverseFixedEndpoint.fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall
(EulerTransverseEndpointParameter.affineTrial T hT Q Q₁))
ξ);
AbsolutelyContinuousOnInterval v 0 T ∧ ↑↑((EulerTransverseEndpointCoordinates.coordinateSlope T hT Q Q₁ H c hc hQ hd K hK hH hsmall)
ξ) =ᵐ[EulerTimeLp.timeMeasure T] v ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt v
(↑↑((EulerTransverseEndpointCoordinates.coordinateAcceleration T hT Q Q₁ H c hc hQ hd K hK hH hsmall) ξ) t) t
theorem
EulerFixedEndpointStrong.continuousCoordinateVelocity_eq
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hTpos : 0 < T)
(hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t)
(hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t)
(ξ : U)
(t : ↑(Set.Icc 0 T))
:
((EulerTransverseEndpointCoordinates.continuousCoordinateVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall) ξ) t = EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H
((EulerTransverseFixedEndpoint.fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall
(EulerTransverseEndpointParameter.affineTrial T hT Q Q₁))
ξ)
↑t
The existing bounded reconstruction is this actual stationary coordinate velocity at every time.
theorem
EulerFixedEndpointStrong.historyVelocity_eq
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hTpos : 0 < T)
(hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t)
(hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t)
(ξ : U)
(t : ↑(Set.Icc 0 T))
:
((EulerTransverseEndpointCoordinates.historyVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall) ξ) t = (Q t)
(EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H
((EulerTransverseFixedEndpoint.fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall
(EulerTransverseEndpointParameter.affineTrial T hT Q Q₁))
ξ)
↑t)
theorem
EulerFixedEndpointStrong.continuousCoordinateVelocity_hasDerivWithinAt_generator
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hTpos : 0 < T)
(hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t)
(hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t)
(ξ : U)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt
(EulerVolterraConvolution.extendPath T hT
((EulerTransverseEndpointCoordinates.continuousCoordinateVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall) ξ))
(((EulerTransverseForwardInverse.generator T Q Q₁ c hc hQ) t)
(((EulerTransverseEndpointCoordinates.continuousCoordinateVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall) ξ) t))
(Set.Icc 0 T) ↑t
theorem
EulerFixedEndpointStrong.continuousCoordinateVelocity_eq_forward
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hTpos : 0 < T)
(hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t)
(hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t)
(evolution : EulerLinearDuhamel.Evolution T hT (EulerTransverseForwardInverse.generator T Q Q₁ c hc hQ))
(ξ : U)
(t : ↑(Set.Icc 0 T))
:
((EulerTransverseEndpointCoordinates.continuousCoordinateVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall) ξ) t = (EulerTransverseForwardInverse.coordinates T hT Q Q₁ c hc hQ evolution 0
(((EulerTransverseEndpointCoordinates.continuousCoordinateVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall) ξ)
⟨0, ⋯⟩))
t
The affine-terminal coordinate history coincides with the actual homogeneous forward solver with its own initial velocity.