Classical first-time regularity of the actual endpoint solution. The genuine momentum and Gram inverse construct a continuous physical velocity, which is proved to represent the variational derivative and to be the displacement's within-interval derivative at every time. The endpoint energy operator is therefore the actual projected terminal derivative.

The actual transverse momentum for an initial-zero stationary path whose terminal displacement may be nonzero. A canonical bounded terminal momentum map is obtained from the weak equation and the true time primitive. Its continuous representative and derivative are conclusions, not extra data.

noncomputable def EulerTransverseEndpointMomentum.initialMomentumForcing {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)) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T U)

The literal derivative of Q*η_t for the homogeneous stationary equation.

Equations

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

theorem EulerTransverseEndpointMomentum.initialMomentumForcing_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)) (u : ↥(EulerTimeLp.TimeLp T E)) : ↑↑((initialMomentumForcing T hT Q Q₁ H) u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q₁ t)) (↑↑u t) - (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q t)) ((EulerVolterraConvolution.extendPath T hT H t) (EulerInitialTimePrimitive.initialRealPrimitive T u t))

theorem EulerTransverseEndpointMomentum.initialMomentum_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)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (m : ↑(Set.Icc 0 T) → E) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : U), inner ℝ (m t) ((Q t) x) = 0) (u : ↥(EulerTimeLp.TimeLp T E)) (hu : ∀ (v : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)), inner ℝ u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) u)) ((EulerTransverseVariationalInverse.transversePrimitive T hT m) v) = 0) (v : ↥(EulerTimeLp.TimeLp T U)) (hv : (EulerTerminalTimePrimitive.initialTrace T hT) v = 0) : inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) v = -inner ℝ ((initialMomentumForcing T hT Q Q₁ H) u) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)

The weak derivative identity is extracted from genuine transverse product tests.

noncomputable def EulerTransverseEndpointMomentum.terminalMomentum {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)) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] U

A bounded linear map giving the terminal value of the actual momentum.

Equations

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

noncomputable def EulerTransverseEndpointMomentum.momentumPath {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)) (u : ↥(EulerTimeLp.TimeLp T E)) (t : ℝ) : U

The canonical momentum representative, including both time endpoints.

Equations

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

theorem EulerTransverseEndpointMomentum.momentumPath_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)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (u : ↥(EulerTimeLp.TimeLp T E)) : Continuous (momentumPath T hT Q Q₁ H u)

theorem EulerTransverseEndpointMomentum.momentumPath_absolutelyContinuous {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)) (u : ↥(EulerTimeLp.TimeLp T E)) : AbsolutelyContinuousOnInterval (momentumPath T hT Q Q₁ H u) 0 T

theorem EulerTransverseEndpointMomentum.momentumPath_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)) (u : ↥(EulerTimeLp.TimeLp T E)) : momentumPath T hT Q Q₁ H u T = (terminalMomentum T hT Q Q₁ H) u

theorem EulerTransverseEndpointMomentum.momentumPath_hasDerivAt_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)) (u : ↥(EulerTimeLp.TimeLp T E)) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (momentumPath T hT Q Q₁ H u) (↑↑((initialMomentumForcing T hT Q Q₁ H) u) t) t

theorem EulerTransverseEndpointMomentum.momentum_eq_primitive_add_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)) (hTpos : 0 < 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 ℝ ((initialMomentumForcing T hT Q Q₁ H) u) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)) : EulerTransverseMomentumRegularity.momentum T hT Q u = (EulerTerminalTimePrimitive.primitiveTimeLp T hT) ((initialMomentumForcing T hT Q Q₁ H) u) + EulerTimeWeakDerivative.constantField T hT ((terminalMomentum T hT Q Q₁ H) u)

theorem EulerTransverseEndpointMomentum.momentumPath_ae_of_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)) (hTpos : 0 < 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 ℝ ((initialMomentumForcing T hT Q Q₁ H) u) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)) : ↑↑(EulerTransverseMomentumRegularity.momentum T hT Q u) =ᵐ[EulerTimeLp.timeMeasure T] momentumPath T hT Q Q₁ H u

theorem EulerTransverseEndpointMomentum.endpointDerivative_momentumPath_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)) (hTpos : 0 < T) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (m : ↑(Set.Icc 0 T) → E) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : U), inner ℝ (m t) ((Q t) x) = 0) (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)) (Y : V) : have u := (EulerTransverseEndpointEnergy.endpointDerivative T hT m H K hK hH hsmall L) Y; ↑↑(EulerTransverseMomentumRegularity.momentum T hT Q u) =ᵐ[EulerTimeLp.timeMeasure T] momentumPath T hT Q Q₁ H u

The momentum of the constructed endpoint solution has this actual continuous representative.

The actual Green identity for the constructed stationary transverse path. Its endpoint energy is the terminal momentum paired with terminal coordinates. All time boundary terms are obtained from absolute continuity and the genuine H¹ coordinate reconstruction.

theorem EulerTransverseEndpointGreen.initial_coordinate_green {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 v : ↥(EulerTimeLp.TimeLp T E)) (hweak : ∀ (w : ↥(EulerTimeLp.TimeLp T U)), (EulerTerminalTimePrimitive.initialTrace T hT) w = 0 → inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) w = -inner ℝ ((EulerTransverseEndpointMomentum.initialMomentumForcing T hT Q Q₁ H) u) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) w)) (hvRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T v ↑t) : inner ℝ ((EulerTransverseEndpointEnergy.energyOperator T hT H) u) v = inner ℝ ((EulerTransverseEndpointMomentum.terminalMomentum T hT Q Q₁ H) u) (EulerTransverseInitialCoordinates.initialCoordinates T hT Q c hc hQ v T)

The exact boundary identity for any genuine tangent initial-zero test path.

noncomputable def EulerTransverseEndpointGreen.terminalCoordinates {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 : 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) {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (R : V →L[ℝ] E) : V →L[ℝ] U

The true terminal coordinate map associated with a physical terminal trace.

Equations

• EulerTransverseEndpointGreen.terminalCoordinates T hT Q c hc hQ R = (EulerTransverseGramPath.frameLeftInversePath T Q c hc hQ) ⟨T, ⋯⟩ ∘SL R

theorem EulerTransverseEndpointGreen.dirichletToNeumann_eq_terminalMomentum {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)) {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (hTpos : 0 < T) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑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) (L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (R : V →L[ℝ] E) (hL : ∀ (Y : V) (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (((EulerInitialTimePrimitive.initialPrimitive T hT) (L Y)) t) = 0) (hLT : ∀ (Y : V), ((EulerInitialTimePrimitive.initialPrimitive T hT) (L Y)) ⟨T, ⋯⟩ = R Y) (Y : V) : (EulerTransverseEndpointEnergy.dirichletToNeumann T hT m H K hK hH hsmall L) Y = (ContinuousLinearMap.adjoint (terminalCoordinates T hT Q c hc hQ R)) ((EulerTransverseEndpointMomentum.terminalMomentum T hT Q Q₁ H) ((EulerTransverseEndpointEnergy.endpointDerivative T hT m H K hK hH hsmall L) Y))

The constructed endpoint energy operator is exactly the pulled-back terminal momentum.

theorem EulerTransverseEndpointVelocity.initialCoordinates_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 : 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) (u : ↥(EulerTimeLp.TimeLp T E)) : Continuous (EulerTransverseInitialCoordinates.initialCoordinates T hT Q c hc hQ u)

noncomputable def EulerTransverseEndpointVelocity.coordinateVelocityPath {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

Coordinate velocity path, constructed using extendPath.

Equations

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

noncomputable def EulerTransverseEndpointVelocity.physicalVelocityPath {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 : ℝ) : E

Physical velocity path, constructed using extendPath.

Equations

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

theorem EulerTransverseEndpointVelocity.coordinateVelocityPath_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 (coordinateVelocityPath T hT Q Q₁ c hc hQ H u)

theorem EulerTransverseEndpointVelocity.physicalVelocityPath_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 (physicalVelocityPath T hT Q Q₁ c hc hQ H u)

theorem EulerTransverseEndpointVelocity.physicalVelocityPath_momentum {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 : ℝ) : (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q t)) (physicalVelocityPath T hT Q Q₁ c hc hQ H u t) = EulerTransverseEndpointMomentum.momentumPath T hT Q Q₁ H u t

The continuous velocity has the exact prescribed momentum at every time.

theorem EulerTransverseEndpointVelocity.coordinateVelocityPath_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)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (hTpos : 0 < 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) : ↑↑(EulerTransverseInitialCoordinates.initialCoordinateDerivative T hT Q Q₁ c hc hQ u) =ᵐ[EulerTimeLp.timeMeasure T] coordinateVelocityPath T hT Q Q₁ c hc hQ H u

theorem EulerTransverseEndpointVelocity.physicalVelocityPath_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)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (hTpos : 0 < 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) : ↑↑u =ᵐ[EulerTimeLp.timeMeasure T] physicalVelocityPath T hT Q Q₁ c hc hQ H u

The continuous physical velocity represents the original variational derivative.

theorem EulerTransverseEndpointVelocity.initialPrimitive_hasDerivWithinAt_of_continuous {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T E)) (f : ℝ → E) (hf : Continuous f) (hu : ↑↑u =ᵐ[EulerTimeLp.timeMeasure T] f) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerInitialTimePrimitive.initialRealPrimitive T u) (f ↑t) (Set.Icc 0 T) ↑t

A continuous representative of a genuine L² derivative differentiates its initial primitive at every time, including the one-sided endpoint derivative.

theorem EulerTransverseEndpointVelocity.stationary_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)) (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)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (hTpos : 0 < 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 (EulerInitialTimePrimitive.initialRealPrimitive T u) (physicalVelocityPath T hT Q Q₁ c hc hQ H u ↑t) (Set.Icc 0 T) ↑t

theorem EulerTransverseEndpointVelocity.dirichletToNeumann_eq_terminal_velocity {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)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (hTpos : 0 < 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) (L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (R : V →L[ℝ] E) (hL : ∀ (Y : V) (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (((EulerInitialTimePrimitive.initialPrimitive T hT) (L Y)) t) = 0) (hLT : ∀ (Y : V), ((EulerInitialTimePrimitive.initialPrimitive T hT) (L Y)) ⟨T, ⋯⟩ = R Y) (Y : V) : (EulerTransverseEndpointEnergy.dirichletToNeumann T hT m H K hK hH hsmall L) Y = (ContinuousLinearMap.adjoint R) (physicalVelocityPath T hT Q Q₁ c hc hQ H ((EulerTransverseEndpointEnergy.endpointDerivative T hT m H K hK hH hsmall L) Y) T)

The actual endpoint energy operator is the physical terminal derivative paired with the prescribed physical terminal trace map.

theorem EulerTransverseEndpointVelocity.endpointDisplacement_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)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (hTpos : 0 < 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) (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 (EulerInitialTimePrimitive.initialRealPrimitive T u) (physicalVelocityPath T hT Q Q₁ c hc hQ H u ↑t) (Set.Icc 0 T) ↑t

The derivative used in the endpoint formula is the actual one at every time.