The constructed affine-terminal inverse as a classical coordinate path, and its uniqueness among actual twice differentiable coordinate paths.

The actual continuous-time integral agrees with both Bochner primitive constructions.

theorem EulerTimeContinuousPrimitive.initialPrimitive_pathLp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) : (EulerInitialTimePrimitive.initialPrimitive T hT) (EulerTimeLp.pathLp T hT f) = (EulerContinuousTimeIntegral.integral T hT) f

theorem EulerTimeContinuousPrimitive.initialTrace_pathLp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) : (EulerTerminalTimePrimitive.initialTrace T hT) (EulerTimeLp.pathLp T hT f) = -((EulerContinuousTimeIntegral.integral T hT) f) ⟨T, ⋯⟩

theorem EulerTimeContinuousPrimitive.primitive_eq_path {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (p q : C(↑(Set.Icc 0 T), E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t) (hzero : p ⟨0, ⋯⟩ = 0) : (EulerInitialTimePrimitive.initialPrimitive T hT) (EulerTimeLp.pathLp T hT q) = p

theorem EulerTimeContinuousPrimitive.initialTrace_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (p q : C(↑(Set.Icc 0 T), E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t) (hzero : p ⟨0, ⋯⟩ = 0) (hterminal : p ⟨T, ⋯⟩ = 0) : (EulerTerminalTimePrimitive.initialTrace T hT) (EulerTimeLp.pathLp T hT q) = 0

theorem EulerTimeContinuousPrimitive.primitiveTimeLp_eq_pathLp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (p q : C(↑(Set.Icc 0 T), E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t) (hzero : p ⟨0, ⋯⟩ = 0) (hterminal : p ⟨T, ⋯⟩ = 0) : (EulerTerminalTimePrimitive.primitiveTimeLp T hT) (EulerTimeLp.pathLp T hT q) = EulerTimeLp.pathLp T hT p

theorem EulerTimeContinuousPrimitive.pathLp_injective {E : Type u_1} [NormedAddCommGroup E] (T : ℝ) (hT : 0 ≤ T) (hTpos : 0 < T) : Function.Injective (EulerTimeLp.pathLp T hT)

Boundary uniqueness for the literal moving-frame coordinate equation. The proof passes through the physical displacement and the already proved short-time energy coercivity, including the source identity Q'' = -H Q.

Uniqueness for an actual twice differentiable zero-endpoint path follows from the source short-time energy coercivity. The differential residual need only be orthogonal to the displacement, as for a constrained frame equation. No inverse or uniqueness assertion is assumed.

theorem EulerTimeEndpointEnergyUniqueness.zero_of_energy_equation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (hTpos : 0 < T) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (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) (p u q : C(↑(Set.Icc 0 T), E)) (hp : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (u t) (Set.Icc 0 T) ↑t) (hu : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT u) (q t) (Set.Icc 0 T) ↑t) (hzero : p ⟨0, ⋯⟩ = 0) (hterminal : p ⟨T, ⋯⟩ = 0) (heq : ∀ (t : ↑(Set.Icc 0 T)), inner ℝ (q t + (H t) (p t)) (p t) = 0) : p = 0 ∧ u = 0

def EulerFrameEndpointUniqueness.applyPath {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] {T : ℝ} (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (z : C(↑(Set.Icc 0 T), U)) : C(↑(Set.Icc 0 T), E)

Apply path, given by ⟨fun t => Q t (z t),Q.continuous.clm_apply z.continuous⟩.

Equations

• EulerFrameEndpointUniqueness.applyPath Q z = { toFun := fun (t : ↑(Set.Icc 0 T)) => (Q t) (z t), continuous_toFun := ⋯ }

theorem EulerFrameEndpointUniqueness.applyPath_hasDerivWithinAt {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (z v : C(↑(Set.Icc 0 T), U)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (hz : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT z) (v t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (applyPath Q z)) ((applyPath Q₁ z + applyPath Q v) t) (Set.Icc 0 T) ↑t

theorem EulerFrameEndpointUniqueness.zero_of_projected_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) (hTpos : 0 < T) (Q 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) (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) (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) (z v a : C(↑(Set.Icc 0 T), U)) (hz : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT z) (v t) (Set.Icc 0 T) ↑t) (hv : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT v) (a t) (Set.Icc 0 T) ↑t) (hzero : z ⟨0, ⋯⟩ = 0) (hterminal : z ⟨T, ⋯⟩ = 0) (heq : ∀ (t : ↑(Set.Icc 0 T)), (EulerTransverseGramInverse.gram (Q t)) (a t) = (ContinuousLinearMap.adjoint (Q t)) (-2 • (Q₁ t) (v t))) : z = 0 ∧ v = 0

theorem EulerFrameEndpointUniqueness.unique_of_projected_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) (hTpos : 0 < T) (Q 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) (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) (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) (z v a w r b : C(↑(Set.Icc 0 T), U)) (hz : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT z) (v t) (Set.Icc 0 T) ↑t) (hv : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT v) (a t) (Set.Icc 0 T) ↑t) (hw : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT w) (r t) (Set.Icc 0 T) ↑t) (hr : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT r) (b t) (Set.Icc 0 T) ↑t) (hzero : z ⟨0, ⋯⟩ = w ⟨0, ⋯⟩) (hterminal : z ⟨T, ⋯⟩ = w ⟨T, ⋯⟩) (heq : ∀ (t : ↑(Set.Icc 0 T)), (EulerTransverseGramInverse.gram (Q t)) (a t) = (ContinuousLinearMap.adjoint (Q t)) (-2 • (Q₁ t) (v t))) (heq' : ∀ (t : ↑(Set.Icc 0 T)), (EulerTransverseGramInverse.gram (Q t)) (b t) = (ContinuousLinearMap.adjoint (Q t)) (-2 • (Q₁ t) (r t))) : z = w ∧ v = r

noncomputable def EulerFixedEndpointClassical.displacement {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 →L[ℝ] C(↑(Set.Icc 0 T), U)

Displacement, given by (initialPrimitive T hT).comp (coordinateSlope T hT Q Q₁ H c hc hQ hd K hK hH hsmall).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerFixedEndpointClassical.acceleration {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 →L[ℝ] C(↑(Set.Icc 0 T), U)

Acceleration as an element of U →L[ℝ] C(Icc (0 : ℝ) T,U).

Equations

• One or more equations did not get rendered due to their size.

theorem EulerFixedEndpointClassical.displacement_initial {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) (Y : U) : ((displacement T hT Q Q₁ H c hc hQ hd K hK hH hsmall) Y) ⟨0, ⋯⟩ = 0

theorem EulerFixedEndpointClassical.displacement_terminal {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) (Y : U) : ((displacement T hT Q Q₁ H c hc hQ hd K hK hH hsmall) Y) ⟨T, ⋯⟩ = Y

theorem EulerFixedEndpointClassical.velocity_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) (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) (Y : U) : ↑↑((EulerTransverseEndpointCoordinates.coordinateSlope T hT Q Q₁ H c hc hQ hd K hK hH hsmall) Y) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT ((EulerTransverseEndpointCoordinates.continuousCoordinateVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall) Y)

theorem EulerFixedEndpointClassical.displacement_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)) (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) (Y : U) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT ((displacement T hT Q Q₁ H c hc hQ hd K hK hH hsmall) Y)) (((EulerTransverseEndpointCoordinates.continuousCoordinateVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall) Y) t) (Set.Icc 0 T) ↑t

theorem EulerFixedEndpointClassical.velocity_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)) (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) (Y : 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) Y)) (((acceleration T hT Q Q₁ H c hc hQ hd K hK hH hsmall) Y) t) (Set.Icc 0 T) ↑t

theorem EulerFixedEndpointClassical.projected_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) (Y : U) (t : ↑(Set.Icc 0 T)) : (EulerTransverseGramInverse.gram (Q t)) (((acceleration T hT Q Q₁ H c hc hQ hd K hK hH hsmall) Y) t) = (ContinuousLinearMap.adjoint (Q t)) (-2 • (Q₁ t) (((EulerTransverseEndpointCoordinates.continuousCoordinateVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall) Y) t))

theorem EulerFixedEndpointClassical.unique {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) (Y : U) (z v a : C(↑(Set.Icc 0 T), U)) (hz : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT z) (v t) (Set.Icc 0 T) ↑t) (hv : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT v) (a t) (Set.Icc 0 T) ↑t) (hz0 : z ⟨0, ⋯⟩ = 0) (hzT : z ⟨T, ⋯⟩ = Y) (heq : ∀ (t : ↑(Set.Icc 0 T)), (EulerTransverseGramInverse.gram (Q t)) (a t) = (ContinuousLinearMap.adjoint (Q t)) (-2 • (Q₁ t) (v t))) : z = (displacement T hT Q Q₁ H c hc hQ hd K hK hH hsmall) Y ∧ v = (EulerTransverseEndpointCoordinates.continuousCoordinateVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall) Y