The actual nonzero-terminal stationary displacement satisfies source (10). Its coordinate velocity solves the very same homogeneous first-order generator used by the packet's forward inverse. The identity is proved by differentiating the constructed momentum, including the endpoint derivatives.
Classical differentiation of the nonzero-terminal stationary coordinates. The continuous physical velocity upgrades the weak momentum derivative to an every-time derivative; the actual Gram inverse then differentiates the coordinate velocity. These are properties of the constructed weak solution.
noncomputable def
EulerTransverseEndpointDifferentiation.momentumDerivativePath
{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))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(u : ↥(EulerTimeLp.TimeLp T E))
(t : ℝ)
:
U
Momentum derivative path as an element of U.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransverseEndpointDifferentiation.momentumDerivativePath_continuous
{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))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(u : ↥(EulerTimeLp.TimeLp T E))
:
Continuous (momentumDerivativePath T hT Q Q₁ c hc hQ H u)
theorem
EulerTransverseEndpointDifferentiation.initialCoordinates_eq_initialPrimitive
{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))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(u : ↥(EulerTimeLp.TimeLp T E))
(t : ↑(Set.Icc 0 T))
:
EulerTransverseInitialCoordinates.initialCoordinates T hT Q c hc hQ u ↑t = EulerInitialTimePrimitive.initialRealPrimitive T
(EulerTransverseInitialCoordinates.initialCoordinateDerivative T hT Q Q₁ c hc hQ u) ↑t
theorem
EulerTransverseEndpointDifferentiation.momentumDerivativePath_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))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(hTpos : 0 < T)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(u : ↥(EulerTimeLp.TimeLp T E))
(hweak :
∀ (v : ↥(EulerTimeLp.TimeLp T U)),
(EulerTerminalTimePrimitive.initialTrace T hT) v = 0 →
inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) v = -inner ℝ ((EulerTransverseEndpointMomentum.initialMomentumForcing T hT Q Q₁ H) u)
((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v))
(huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t)
:
↑↑((EulerTransverseEndpointMomentum.initialMomentumForcing T hT Q Q₁ H) u) =ᵐ[EulerTimeLp.timeMeasure T] momentumDerivativePath T hT Q Q₁ c hc hQ H u
theorem
EulerTransverseEndpointDifferentiation.momentumPath_hasDerivWithinAt
{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))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(hTpos : 0 < T)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(u : ↥(EulerTimeLp.TimeLp T E))
(hweak :
∀ (v : ↥(EulerTimeLp.TimeLp T U)),
(EulerTerminalTimePrimitive.initialTrace T hT) v = 0 →
inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) v = -inner ℝ ((EulerTransverseEndpointMomentum.initialMomentumForcing T hT Q Q₁ H) u)
((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v))
(huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt (EulerTransverseEndpointMomentum.momentumPath T hT Q Q₁ H u)
(momentumDerivativePath T hT Q Q₁ c hc hQ H u ↑t) (Set.Icc 0 T) ↑t
theorem
EulerTransverseEndpointDifferentiation.initialCoordinates_hasDerivWithinAt
{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))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(hTpos : 0 < T)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(u : ↥(EulerTimeLp.TimeLp T E))
(hweak :
∀ (v : ↥(EulerTimeLp.TimeLp T U)),
(EulerTerminalTimePrimitive.initialTrace T hT) v = 0 →
inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) v = -inner ℝ ((EulerTransverseEndpointMomentum.initialMomentumForcing T hT Q Q₁ H) u)
((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v))
(huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t)
(t : ↑(Set.Icc 0 T))
:
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
noncomputable def
EulerTransverseEndpointDifferentiation.rawCoordinateAcceleration
{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₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(u : ↥(EulerTimeLp.TimeLp T E))
(t : ℝ)
:
U
Raw coordinate acceleration, constructed using extendPath.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransverseEndpointDifferentiation.coordinateVelocityPath_hasDerivWithinAt_raw
{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₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(hTpos : 0 < T)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t)
(u : ↥(EulerTimeLp.TimeLp T E))
(hweak :
∀ (v : ↥(EulerTimeLp.TimeLp T U)),
(EulerTerminalTimePrimitive.initialTrace T hT) v = 0 →
inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) v = -inner ℝ ((EulerTransverseEndpointMomentum.initialMomentumForcing T hT Q Q₁ H) u)
((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v))
(huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt (EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H u)
(rawCoordinateAcceleration T hT Q Q₁ Q₂ c hc hQ H u ↑t) (Set.Icc 0 T) ↑t
theorem
EulerTransverseEndpointDifferentiation.coordinateMomentum_identity
{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))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(u : ↥(EulerTimeLp.TimeLp T E))
(t : ℝ)
:
(EulerVolterraConvolution.extendPath T hT (EulerTransverseGramPath.gramPath T Q) t)
(EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H u t) + (EulerVolterraConvolution.extendPath T hT (EulerTransverseStrongAlgebra.mixedPath T Q Q₁) t)
(EulerTransverseInitialCoordinates.initialCoordinates T hT Q c hc hQ u t) = EulerTransverseEndpointMomentum.momentumPath T hT Q Q₁ H u t
The defining inverse-Gram relation is an actual pointwise momentum identity.
theorem
EulerTransverseEndpointEquation.rawCoordinateAcceleration_projected
{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₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(hTpos : 0 < T)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑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 : ↥(EulerTimeLp.TimeLp T E))
(hweak :
∀ (v : ↥(EulerTimeLp.TimeLp T U)),
(EulerTerminalTimePrimitive.initialTrace T hT) v = 0 →
inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) v = -inner ℝ ((EulerTransverseEndpointMomentum.initialMomentumForcing T hT Q Q₁ H) u)
((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v))
(huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t)
(t : ↑(Set.Icc 0 T))
:
(EulerTransverseGramInverse.gram (Q t))
(EulerTransverseEndpointDifferentiation.rawCoordinateAcceleration T hT Q Q₁ Q₂ c hc hQ H u ↑t) = (ContinuousLinearMap.adjoint (Q t))
(0 - 2 • (Q₁ t) (EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H u ↑t))
theorem
EulerTransverseEndpointEquation.rawCoordinateAcceleration_eq_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₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(hTpos : 0 < T)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑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 : ↥(EulerTimeLp.TimeLp T E))
(hweak :
∀ (v : ↥(EulerTimeLp.TimeLp T U)),
(EulerTerminalTimePrimitive.initialTrace T hT) v = 0 →
inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) v = -inner ℝ ((EulerTransverseEndpointMomentum.initialMomentumForcing T hT Q Q₁ H) u)
((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v))
(huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t)
(t : ↑(Set.Icc 0 T))
:
EulerTransverseEndpointDifferentiation.rawCoordinateAcceleration T hT Q Q₁ Q₂ c hc hQ H u ↑t = ((EulerTransverseForwardInverse.generator T Q Q₁ c hc hQ) t)
(EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H u ↑t)
theorem
EulerTransverseEndpointEquation.coordinateVelocityPath_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₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(hTpos : 0 < T)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑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 : ↥(EulerTimeLp.TimeLp T E))
(hweak :
∀ (v : ↥(EulerTimeLp.TimeLp T U)),
(EulerTerminalTimePrimitive.initialTrace T hT) v = 0 →
inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) v = -inner ℝ ((EulerTransverseEndpointMomentum.initialMomentumForcing T hT Q Q₁ H) u)
((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v))
(huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t)
(t : ↑(Set.Icc 0 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 actual coordinate displacement, written as the first-order equation for its genuine derivative.
theorem
EulerTransverseEndpointEquation.coordinateVelocity_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₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(hTpos : 0 < T)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑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 : ↥(EulerTimeLp.TimeLp T E))
(hweak :
∀ (v : ↥(EulerTimeLp.TimeLp T U)),
(EulerTerminalTimePrimitive.initialTrace T hT) v = 0 →
inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) v = -inner ℝ ((EulerTransverseEndpointMomentum.initialMomentumForcing T hT Q Q₁ H) u)
((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v))
(huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t)
(evolution : EulerLinearDuhamel.Evolution T hT (EulerTransverseForwardInverse.generator T Q Q₁ c hc hQ))
(t : ↑(Set.Icc 0 T))
:
EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H u ↑t = (EulerTransverseForwardInverse.coordinates T hT Q Q₁ c hc hQ evolution 0
(EulerTransverseEndpointVelocity.coordinateVelocityPath T hT Q Q₁ c hc hQ H u 0))
t
The stationary history velocity is the same actual solution as the packet's homogeneous forward inverse, whenever both are placed on this time interval.
theorem
EulerTransverseEndpointEquation.endpoint_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₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(hTpos : 0 < T)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑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)
(m : ↑(Set.Icc 0 T) → E)
(hm : ∀ (t : ↑(Set.Icc 0 T)) (x : U), inner ℝ (m t) ((Q t) x) = 0)
(hRange : ∀ (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m t) η = 0 → ∃ (x : U), (Q t) x = η)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
(hL : ∀ (Y : V) (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (((EulerInitialTimePrimitive.initialPrimitive T hT) (L Y)) t) = 0)
(Y : V)
(t : ↑(Set.Icc 0 T))
:
have u := (EulerTransverseEndpointEnergy.endpointDerivative T hT m H K hK hH hsmall L) Y;
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
The nonzero-terminal inverse used in activation has genuine first and second coordinate derivatives satisfying the source's homogeneous equation.