The actual zero-endpoint transverse displacement inverse

We use the derivative of the physical displacement as the Hilbert-space variable. Terminal integration supplies the displacement. Its initial trace and its moving normal component are bounded linear constraints, hence define a closed Hilbert subspace. The kinetic energy is exactly the squared norm on this space; no norm equivalence or pre-existing differential inverse is assumed.

This constructs the weak transverse inverse in source lines 172--184. The coordinate identity η = F R ξ and strong coordinate evolution require the separate frame and regularity arguments; they are not assumed in this file.

Recovering the source's transverse coordinates

The moving plane with normal (F⁻¹)* m₀ is exactly the image under F of the fixed plane m₀⊥. Orthogonal projection gives a bounded coordinate map, and on the moving plane its reconstruction is the identity. These are coefficient identities, not assumptions about a differential inverse.

@[reducible, inline]

noncomputable abbrev EulerTransverseFrameCoordinates.referencePlane {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m₀ : E) : Submodule ℝ E

The fixed reference transverse plane.

Equations

• EulerTransverseFrameCoordinates.referencePlane m₀ = (ℝ ∙ m₀)ᗮ

noncomputable def EulerTransverseFrameCoordinates.movingNormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (F : E ≃L[ℝ] E) (m₀ : E) : E

The actual pulled-back normal used by the packet construction.

Equations

• EulerTransverseFrameCoordinates.movingNormal F m₀ = (ContinuousLinearMap.adjoint ↑F.symm) m₀

noncomputable def EulerTransverseFrameCoordinates.coordinates {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (F : E ≃L[ℝ] E) (m₀ : E) : E →L[ℝ] ↥(referencePlane m₀)

Bounded recovery of fixed-plane coordinates from a physical displacement.

Equations

• EulerTransverseFrameCoordinates.coordinates F m₀ = (EulerTransverseFrameCoordinates.referencePlane m₀).orthogonalProjectionOnto ∘SL ↑F.symm

theorem EulerTransverseFrameCoordinates.tangent_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (F : E ≃L[ℝ] E) (m₀ η : E) : inner ℝ (movingNormal F m₀) η = 0 ↔ F.symm η ∈ referencePlane m₀

Moving tangency is exactly fixed-plane membership after applying F⁻¹.

theorem EulerTransverseFrameCoordinates.reconstruct {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (F : E ≃L[ℝ] E) (m₀ η : E) (hη : inner ℝ (movingNormal F m₀) η = 0) : F ↑((coordinates F m₀) η) = η

Reconstructing a tangent displacement from its recovered coordinates is exact.

theorem EulerTransverseFrameCoordinates.coordinates_leftInverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (F : E ≃L[ℝ] E) (m₀ : E) (ξ : ↥(referencePlane m₀)) : (coordinates F m₀) (F ↑ξ) = ξ

The coordinate map is a left inverse to F restricted to the reference plane.

theorem EulerTransverseFrameCoordinates.coordinates_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (F : E ≃L[ℝ] E) (m₀ η : E) : ‖(coordinates F m₀) η‖ ≤ ‖↑F.symm‖ * ‖η‖

The coordinate map has the expected polynomial bound from the inverse frame.

noncomputable def EulerTransverseFrameCoordinates.frameCoordinates {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (F : E ≃L[ℝ] E) (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(referencePlane m₀)) : E →L[ℝ] U

Any orthonormal identification with the fixed plane gives the source's R⊥ coordinates.

Equations

• EulerTransverseFrameCoordinates.frameCoordinates F m₀ R = ↑↑R.symm ∘SL EulerTransverseFrameCoordinates.coordinates F m₀

theorem EulerTransverseFrameCoordinates.frame_reconstruct {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (F : E ≃L[ℝ] E) (m₀ η : E) (R : U ≃ₗᵢ[ℝ] ↥(referencePlane m₀)) (hη : inner ℝ (movingNormal F m₀) η = 0) : F ↑(R ((frameCoordinates F m₀ R) η)) = η

The full source reconstruction η = F R⊥ ξ follows from moving tangency.

theorem EulerTransverseFrameCoordinates.frameCoordinates_norm {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (F : E ≃L[ℝ] E) (m₀ η : E) (R : U ≃ₗᵢ[ℝ] ↥(referencePlane m₀)) : ‖(frameCoordinates F m₀ R) η‖ ≤ ‖↑F.symm‖ * ‖η‖

Passing to an orthonormal coordinate basis has no extra norm cost.

noncomputable def EulerTransverseFrameCoordinates.coordinatePath {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] {X : Type u_3} [TopologicalSpace X] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(referencePlane m₀)) (A : C(X, E →L[ℝ] E)) (η : C(X, E)) : C(X, U)

Applying a continuous inverse-frame path produces actual continuous transverse coordinates, not separate incompatible pointwise choices.

Equations

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

theorem EulerTransverseFrameCoordinates.coordinatePath_reconstruct {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] {X : Type u_3} [TopologicalSpace X] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(referencePlane m₀)) (F : X → E ≃L[ℝ] E) (A : C(X, E →L[ℝ] E)) (hA : ∀ (t : X), A t = ↑(F t).symm) (η : C(X, E)) (hη : ∀ (t : X), inner ℝ (movingNormal (F t) m₀) (η t) = 0) (t : X) : (F t) ↑(R ((coordinatePath m₀ R A η) t)) = η t

The recovered continuous coordinates reconstruct every tangent displacement.

theorem EulerTransverseFrameCoordinates.coordinatePath_zero_at {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] {X : Type u_3} [TopologicalSpace X] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(referencePlane m₀)) (A : C(X, E →L[ℝ] E)) (η : C(X, E)) (t : X) (hη : η t = 0) : (coordinatePath m₀ R A η) t = 0

Zero endpoint displacements give zero endpoint coordinates.

theorem EulerTransverseFrameCoordinates.coordinatePath_norm {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] {X : Type u_3} [TopologicalSpace X] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(referencePlane m₀)) (A : C(X, E →L[ℝ] E)) (η : C(X, E)) (t : X) : ‖(coordinatePath m₀ R A η) t‖ ≤ ‖A t‖ * ‖η t‖

Pointwise coordinate control only pays the actual inverse-frame norm.

def EulerTransverseVariationalInverse.transverseDerivatives {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) : Submodule ℝ ↥(EulerTimeLp.TimeLp T E)

Derivatives of actual zero-endpoint displacements tangent to the moving plane.

Equations

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

theorem EulerTransverseVariationalInverse.transverseDerivatives_closed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) : IsClosed ↑(transverseDerivatives T hT m)

The two endpoint and moving tangency conditions are closed constraints.

instance EulerTransverseVariationalInverse.transverseDerivatives_complete {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) : CompleteSpace ↥(transverseDerivatives T hT m)

Closedness supplies completeness for the actual displacement-derivative space.

theorem EulerTransverseVariationalInverse.transverseDerivatives_integral_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (u : ↥(transverseDerivatives T hT m)) : ∫ (t : ℝ) in 0..T, ↑↑↑u t = 0

The zero initial trace is exactly the zero-mean condition on the time derivative.

theorem EulerTransverseVariationalInverse.derivative_mem_of_ac {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (u : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑u t) t) (hzero : η 0 = 0) (hterminal : η T = 0) (htangent : ∀ (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (η ↑t) = 0) : u ∈ transverseDerivatives T hT m

Every genuine absolutely continuous zero-endpoint transverse path with an L² derivative belongs to this Hilbert model. Thus the test space is not an assumed family of already solved displacements.

noncomputable def EulerTransverseVariationalInverse.transversePrimitive {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) : ↥(transverseDerivatives T hT m) →L[ℝ] ↥(EulerTimeLp.TimeLp T E)

The actual terminal primitive restricted to the transverse derivative space.

Equations

• EulerTransverseVariationalInverse.transversePrimitive T hT m = EulerTerminalTimePrimitive.primitiveTimeLp T hT ∘SL (EulerTransverseVariationalInverse.transverseDerivatives T hT m).subtypeL

theorem EulerTransverseVariationalInverse.transversePrimitive_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (u : ↥(transverseDerivatives T hT m)) : ‖(transversePrimitive T hT m) u‖ ^ 2 ≤ T ^ 2 / 2 * ‖u‖ ^ 2

The sharp time Poincaré bound holds on the actual transverse space.

theorem EulerTransverseVariationalInverse.transversePrimitive_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) : ‖transversePrimitive T hT m‖ ≤ T

A convenient polynomial operator bound for the terminal primitive.

noncomputable def EulerTransverseVariationalInverse.transverseSolver {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(transverseDerivatives T hT m)

The actual transverse forcing-to-derivative map, constructed from the primitive and the given time-dependent Hessian.

Equations

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

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

The continuous displacement is constructed by integrating its solved derivative.

Equations

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

theorem EulerTransverseVariationalInverse.transverseDisplacement_initial {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) (f : ↥(EulerTimeLp.TimeLp T E)) : ((transverseDisplacement T hT m H K hK hH hsmall) f) ⟨0, ⋯⟩ = 0

The solved displacement vanishes at the initial endpoint.

theorem EulerTransverseVariationalInverse.transverseDisplacement_terminal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) (f : ↥(EulerTimeLp.TimeLp T E)) : ((transverseDisplacement T hT m H K hK hH hsmall) f) ⟨T, ⋯⟩ = 0

The solved displacement vanishes at the terminal endpoint.

theorem EulerTransverseVariationalInverse.transverseDisplacement_tangent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) (f : ↥(EulerTimeLp.TimeLp T E)) (t : ↑(Set.Icc 0 T)) : inner ℝ (m t) (((transverseDisplacement T hT m H K hK hH hsmall) f) t) = 0

The solved displacement belongs to the actual moving transverse plane.

theorem EulerTransverseVariationalInverse.transverseDisplacement_hasDerivAt_ae {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) (f : ↥(EulerTimeLp.TimeLp T E)) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (EulerTerminalTimePrimitive.realPrimitive T ↑((transverseSolver T hT m H K hK hH hsmall) f)) (↑↑↑((transverseSolver T hT m H K hK hH hsmall) f) t) t

The derivative of the constructed displacement is the solved L² field, as an actual almost-everywhere derivative of its continuous real-time representative.

theorem EulerTransverseVariationalInverse.transverseSolver_weak {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) (f : ↥(EulerTimeLp.TimeLp T E)) (v : ↥(transverseDerivatives T hT m)) : have u := (transverseSolver T hT m H K hK hH hsmall) f; inner ℝ ↑u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((transversePrimitive T hT m) u)) ((transversePrimitive T hT m) v) = -inner ℝ f ((transversePrimitive T hT m) v)

The actual weak transverse displacement equation, tested against every zero-endpoint displacement in the same moving plane.

theorem EulerTransverseVariationalInverse.transverseSolver_unique {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) (f : ↥(EulerTimeLp.TimeLp T E)) (u : ↥(transverseDerivatives T hT m)) (hu : ∀ (v : ↥(transverseDerivatives T hT m)), inner ℝ ↑u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((transversePrimitive T hT m) u)) ((transversePrimitive T hT m) v) = -inner ℝ f ((transversePrimitive T hT m) v)) : u = (transverseSolver T hT m H K hK hH hsmall) f

The constructed weak inverse is unique in the actual transverse displacement space.

theorem EulerTransverseVariationalInverse.transverseSolver_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) (f : ↥(EulerTimeLp.TimeLp T E)) : ‖(transverseSolver T hT m H K hK hH hsmall) f‖ ≤ 2 * T * ‖f‖

The solved derivative has a polynomial finite-time bound, with no exponential in H.

@[simp]

theorem EulerTransverseVariationalInverse.transverseDisplacement_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) : (transverseDisplacement T hT m H K hK hH hsmall) 0 = 0

Zero forcing has zero displacement, the pointwise-in-label support preservation property.

theorem EulerTransverseVariationalInverse.transverseDisplacement_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) (f : ↥(EulerTimeLp.TimeLp T E)) : (transverseDisplacement T hT m H K hK hH hsmall) (-f) = -(transverseDisplacement T hT m H K hK hH hsmall) f

The inverse preserves sign, hence oddness in a parameter with unchanged coefficients.

theorem EulerTransverseVariationalInverse.transverseDisplacement_integral_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (f : α → ↥(EulerTimeLp.TimeLp T E)) (hf : MeasureTheory.Integrable f μ) (hmean : ∫ (a : α), f a ∂μ = 0) : ∫ (a : α), (transverseDisplacement T hT m H K hK hH hsmall) (f a) ∂μ = 0

A zero angle mean of the forcing gives a zero angle mean of the displacement. The measure can be the normalized periodic angle measure; coefficients are fixed in this parameter.

theorem EulerTransverseVariationalInverse.existsUnique_transverse_weak_solution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (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) (f : ↥(EulerTimeLp.TimeLp T E)) : ∃! u : ↥(transverseDerivatives T hT m), ∀ (v : ↥(transverseDerivatives T hT m)), inner ℝ ↑u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((transversePrimitive T hT m) u)) ((transversePrimitive T hT m) v) = -inner ℝ f ((transversePrimitive T hT m) v)

Existence and uniqueness follow from the actual sharp time primitive estimate, the pointwise potential bound, and closed transverse constraints.

theorem EulerTransverseVariationalInverse.exists_transverse_frame_displacement {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 : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (F : ↑(Set.Icc 0 T) → E ≃L[ℝ] E) (A : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hA : ∀ (t : ↑(Set.Icc 0 T)), A t = ↑(F t).symm) (f : ↥(EulerTimeLp.TimeLp T E)) : have mF := fun (t : ↑(Set.Icc 0 T)) => EulerTransverseFrameCoordinates.movingNormal (F t) m₀; ∃ (u : ↥(transverseDerivatives T hT mF)) (η : C(↑(Set.Icc 0 T), E)) (ξ : C(↑(Set.Icc 0 T), U)), η = (EulerTerminalTimePrimitive.terminalPrimitive T hT) ↑u ∧ η ⟨0, ⋯⟩ = 0 ∧ η ⟨T, ⋯⟩ = 0 ∧ ξ ⟨0, ⋯⟩ = 0 ∧ ξ ⟨T, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 T)), (F t) ↑(R (ξ t)) = η t) ∧ ‖u‖ ≤ 2 * T * ‖f‖ ∧ ∀ (v : ↥(transverseDerivatives T hT mF)), inner ℝ ↑u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((transversePrimitive T hT mF) u)) ((transversePrimitive T hT mF) v) = -inner ℝ f ((transversePrimitive T hT mF) v)

The actual weak inverse has the source's form η = F R⊥ ξ, with continuous coordinates and both endpoint conditions. The frame is prescribed coefficient data; neither a displacement nor a differential inverse is supplied.