The actual endpoint energy in the activation argument. Paths are genuine initial-zero Bochner H¹ paths, and the zero-terminal correction is solved in the existing closed transverse derivative space. Symmetry, positivity and minimum energy are conclusions of the construction.

The endpoint Schur complement of a coercive quadratic form. The stationary extension is constructed by the inverse of the form on the closed zero-trace space. No stationary extension or Dirichlet-to-Neumann map is an input.

noncomputable def EulerDirichletEndpointReduction.correction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) : E →L[ℝ] ↥S

The zero-trace correction obtained by a genuine coercive inverse.

Equations

• EulerDirichletEndpointReduction.correction S A c hc hA = EulerCoerciveProjection.projectedInverse S A c hc hA ∘SL S.orthogonalProjectionOnto ∘SL A

noncomputable def EulerDirichletEndpointReduction.stationaryPart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) : E →L[ℝ] E

Subtract the solved zero-trace correction from any trial extension.

Equations

• EulerDirichletEndpointReduction.stationaryPart S A c hc hA = ContinuousLinearMap.id ℝ E - S.subtypeL ∘SL EulerDirichletEndpointReduction.correction S A c hc hA

theorem EulerDirichletEndpointReduction.stationaryPart_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) (x : E) : (stationaryPart S A c hc hA) x = x - ↑((correction S A c hc hA) x)

theorem EulerDirichletEndpointReduction.correction_equation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) (x : E) (v : ↥S) : inner ℝ (A ↑((correction S A c hc hA) x)) ↑v = inner ℝ (A x) ↑v

theorem EulerDirichletEndpointReduction.stationaryPart_orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) (x : E) (v : ↥S) : inner ℝ (A ((stationaryPart S A c hc hA) x)) ↑v = 0

The constructed extension satisfies all zero-trace stationary equations.

theorem EulerDirichletEndpointReduction.stationaryPart_sub_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) (x : E) : (stationaryPart S A c hc hA) x - x ∈ S

theorem EulerDirichletEndpointReduction.stationaryPart_subspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) (v : ↥S) : (stationaryPart S A c hc hA) ↑v = 0

theorem EulerDirichletEndpointReduction.stationaryPart_eq_of_sub_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) (x y : E) (hxy : x - y ∈ S) : (stationaryPart S A c hc hA) x = (stationaryPart S A c hc hA) y

The actual extension depends only on the terminal class of the trial.

theorem EulerDirichletEndpointReduction.energy_split {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) (hAs : (↑A).IsSymmetric) (x : E) (v : ↥S) : inner ℝ (A ((stationaryPart S A c hc hA) x + ↑v)) ((stationaryPart S A c hc hA) x + ↑v) = inner ℝ (A ((stationaryPart S A c hc hA) x)) ((stationaryPart S A c hc hA) x) + inner ℝ (A ↑v) ↑v

Energy splits orthogonally along the stationary extension and zero-trace variations.

theorem EulerDirichletEndpointReduction.stationaryPart_minimizes {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) (hAs : (↑A).IsSymmetric) (x : E) : inner ℝ (A ((stationaryPart S A c hc hA) x)) ((stationaryPart S A c hc hA) x) ≤ inner ℝ (A x) x

The solved extension minimizes the actual quadratic form in its trace class.

noncomputable def EulerDirichletEndpointReduction.endpointExtension {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) (L : U →L[ℝ] E) : U →L[ℝ] E

A prescribed bounded trial lift followed by the actual stationary projection.

Equations

• EulerDirichletEndpointReduction.endpointExtension S A c hc hA L = EulerDirichletEndpointReduction.stationaryPart S A c hc hA ∘SL L

noncomputable def EulerDirichletEndpointReduction.endpointOperator {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) [CompleteSpace E] (L : U →L[ℝ] E) : U →L[ℝ] U

The operator representing the actual stationary endpoint energy.

Equations

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

theorem EulerDirichletEndpointReduction.endpointOperator_inner {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) [CompleteSpace E] (L : U →L[ℝ] E) (x y : U) : inner ℝ ((endpointOperator S A c hc hA L) x) y = inner ℝ (A ((endpointExtension S A c hc hA L) x)) ((endpointExtension S A c hc hA L) y)

theorem EulerDirichletEndpointReduction.endpointOperator_positive {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) [CompleteSpace E] (hAs : (↑A).IsSymmetric) (L : U →L[ℝ] E) : (endpointOperator S A c hc hA L).IsPositive

Positivity is inherited from the actual displacement form.

theorem EulerDirichletEndpointReduction.endpointOperator_trial_bound {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) [CompleteSpace E] (hAs : (↑A).IsSymmetric) (L : U →L[ℝ] E) (x : U) : inner ℝ ((endpointOperator S A c hc hA L) x) x ≤ inner ℝ (A (L x)) (L x)

Any explicit admissible trial controls the endpoint quadratic form.

theorem EulerDirichletEndpointReduction.positive_norm_le_of_quadratic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (B : E →L[ℝ] E) (hB : B.IsPositive) (C : ℝ) (hC : 0 ≤ C) (hb : ∀ (x : E), inner ℝ (B x) x ≤ C * ‖x‖ ^ 2) : ‖B‖ ≤ C

A nonnegative quadratic-form bound gives the same operator-norm bound.

theorem EulerDirichletEndpointReduction.endpointOperator_norm_le {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Submodule ℝ E) [CompleteSpace ↥S] (A : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (A x) x) [CompleteSpace E] (hAs : (↑A).IsSymmetric) (L : U →L[ℝ] E) (C : ℝ) (hC : 0 ≤ C) (hL : ∀ (x : U), inner ℝ (A (L x)) (L x) ≤ C * ‖x‖ ^ 2) : ‖endpointOperator S A c hc hA L‖ ≤ C

The endpoint norm is controlled by the energy of the trial, without an inverse norm loss.

noncomputable def EulerTransverseEndpointEnergy.energyOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T E)

The physical kinetic-minus-potential form on all initial-zero H¹ paths.

Equations

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

theorem EulerTransverseEndpointEnergy.energyOperator_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (u v : ↥(EulerTimeLp.TimeLp T E)) : inner ℝ ((energyOperator T hT H) u) v = inner ℝ u v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) u)) ((EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) v)

theorem EulerTransverseEndpointEnergy.energyOperator_coercive {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 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) (u : ↥(EulerTimeLp.TimeLp T E)) : 1 / 2 * ‖u‖ ^ 2 ≤ inner ℝ ((energyOperator T hT H) u) u

The source upper Hessian bound and time smallness give actual coercivity, also when the terminal value is nonzero.

theorem EulerTransverseEndpointEnergy.timeMultiplier_symmetric {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hH : ∀ (t : ↑(Set.Icc 0 T)), (↑(H t)).IsSymmetric) : (↑(EulerTimeLp.timeMultiplier T hT H)).IsSymmetric

theorem EulerTransverseEndpointEnergy.energyOperator_symmetric {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hH : ∀ (t : ↑(Set.Icc 0 T)), (↑(H t)).IsSymmetric) : (↑(energyOperator T hT H)).IsSymmetric

theorem EulerTransverseEndpointEnergy.initialPrimitive_transverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (u : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)) (t : ↑(Set.Icc 0 T)) : ((EulerInitialTimePrimitive.initialPrimitive T hT) ↑u) t = ((EulerTerminalTimePrimitive.terminalPrimitive T hT) ↑u) t

theorem EulerTransverseEndpointEnergy.initialPrimitiveTimeLp_transverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (u : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)) : (EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) ↑u = (EulerTransverseVariationalInverse.transversePrimitive T hT m) u

noncomputable def EulerTransverseEndpointEnergy.endpointDerivative {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (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) (L : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)

Solve the zero-endpoint variation problem for an explicit terminal trial lift.

Equations

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

noncomputable def EulerTransverseEndpointEnergy.endpointDisplacement {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (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) (L : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) : U →L[ℝ] C(↑(Set.Icc 0 T), E)

The constructed physical stationary path.

Equations

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

noncomputable def EulerTransverseEndpointEnergy.dirichletToNeumann {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (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) (L : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) : U →L[ℝ] U

The genuine endpoint quadratic form represented by a bounded operator.

Equations

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

theorem EulerTransverseEndpointEnergy.endpointDisplacement_initial {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (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) (L : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (Y : U) : ((endpointDisplacement T hT m H K hK hH hsmall L) Y) ⟨0, ⋯⟩ = 0

theorem EulerTransverseEndpointEnergy.endpointDerivative_sub_mem {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (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) (L : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (Y : U) : (endpointDerivative T hT m H K hK hH hsmall L) Y - L Y ∈ EulerTransverseVariationalInverse.transverseDerivatives T hT m

theorem EulerTransverseEndpointEnergy.endpointDisplacement_terminal {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (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) (L : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (Y : U) : ((endpointDisplacement T hT m H K hK hH hsmall L) Y) ⟨T, ⋯⟩ = ((EulerInitialTimePrimitive.initialPrimitive T hT) (L Y)) ⟨T, ⋯⟩

The stationary correction preserves the actual terminal trace.

theorem EulerTransverseEndpointEnergy.endpointDisplacement_tangent {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (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) (L : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (hL : ∀ (Y : U) (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (((EulerInitialTimePrimitive.initialPrimitive T hT) (L Y)) t) = 0) (Y : U) (t : ↑(Set.Icc 0 T)) : inner ℝ (m t) (((endpointDisplacement T hT m H K hK hH hsmall L) Y) t) = 0

A genuinely tangent trial produces a genuinely tangent stationary path.

theorem EulerTransverseEndpointEnergy.endpointDerivative_weak {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (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) (L : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (Y : U) (v : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)) : inner ℝ ((endpointDerivative T hT m H K hK hH hsmall L) Y) ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) ((endpointDerivative T hT m H K hK hH hsmall L) Y))) ((EulerTransverseVariationalInverse.transversePrimitive T hT m) v) = 0

Every zero-endpoint transverse test satisfies the literal stationary weak equation.

theorem EulerTransverseEndpointEnergy.dirichletToNeumann_inner {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (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) (L : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (Y Z : U) : inner ℝ ((dirichletToNeumann T hT m H K hK hH hsmall L) Y) Z = inner ℝ ((endpointDerivative T hT m H K hK hH hsmall L) Y) ((endpointDerivative T hT m H K hK hH hsmall L) Z) - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) ((endpointDerivative T hT m H K hK hH hsmall L) Y))) ((EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) ((endpointDerivative T hT m H K hK hH hsmall L) Z))

The endpoint pairing is the actual kinetic-minus-potential energy pairing.

theorem EulerTransverseEndpointEnergy.dirichletToNeumann_positive {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (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) (hHs : ∀ (t : ↑(Set.Icc 0 T)), (↑(H t)).IsSymmetric) (L : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) : (dirichletToNeumann T hT m H K hK hH hsmall L).IsPositive

The source endpoint operator is symmetric positive semidefinite.

theorem EulerTransverseEndpointEnergy.dirichletToNeumann_norm_le {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (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) (hHs : ∀ (t : ↑(Set.Icc 0 T)), (↑(H t)).IsSymmetric) (L : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)) (C : ℝ) (hC : 0 ≤ C) (hL : ∀ (Y : U), ‖L Y‖ ^ 2 - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) (L Y))) ((EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) (L Y)) ≤ C * ‖Y‖ ^ 2) : ‖dirichletToNeumann T hT m H K hK hH hsmall L‖ ≤ C

The endpoint norm costs only trial energy, with no inverse or frame norm factor.