Strong transverse evolution from the actual variational solve

The weak momentum identity supplies an actual absolutely continuous momentum. The constructed Gram inverse then upgrades the coordinate derivative to H¹. Differentiating the momentum identity and using Q_tt = -H Q gives the literal projected equation (10), with no assumed acceleration or differential inverse.

noncomputable def EulerTransverseStrongEquation.coordinateSecondDerivative {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 f : ↥(EulerTimeLp.TimeLp T E)) : ↥(EulerTimeLp.TimeLp T U)

The actual candidate second derivative, constructed from L² fields and bounded coefficient multipliers. Its derivative property is proved below.

Equations

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

noncomputable def EulerTransverseStrongEquation.velocityRepresentative {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) (u : ↥(EulerTimeLp.TimeLp T E)) (p : ℝ → U) : ℝ → U

The coordinate velocity recovered from an actual momentum representative.

Equations

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

theorem EulerTransverseStrongEquation.coordinateDerivative_eq_inverse_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) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) (huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerTerminalTimePrimitive.realPrimitive T u ↑t) : EulerTransverseCoordinateRegularity.coordinateDerivative T hT Q Q₁ c hc hQ u = (EulerTimeLp.timeMultiplier T hT (EulerTransverseGramPath.gramInversePath T Q c hc hQ)) (EulerTransverseMomentumRegularity.momentum T hT Q u - (EulerTimeLp.timeMultiplier T hT (EulerTransverseStrongAlgebra.mixedPath T Q Q₁)) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) (EulerTransverseCoordinateRegularity.coordinateDerivative T hT Q Q₁ c hc hQ u)))

The inverse momentum formula recovers the existing coordinate derivative as an equality of genuine Bochner fields.

theorem EulerTransverseStrongEquation.velocityRepresentative_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) (u : ↥(EulerTimeLp.TimeLp T E)) (p : ℝ → U) (t : ℝ) : (EulerVolterraConvolution.extendPath T hT (EulerTransverseGramPath.gramPath T Q) t) (velocityRepresentative T hT Q Q₁ c hc hQ u p t) + (EulerVolterraConvolution.extendPath T hT (EulerTransverseStrongAlgebra.mixedPath T Q Q₁) t) (EulerTransverseCoordinateRegularity.coordinatePrimitive T hT Q c hc hQ u t) = p t

The momentum reconstruction is a pointwise identity at every real time; clamping preserves the actual Gram inverse identities.

theorem EulerTransverseStrongEquation.velocityRepresentative_h1 {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) (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) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (u f : ↥(EulerTimeLp.TimeLp T E)) (huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerTerminalTimePrimitive.realPrimitive T u ↑t) (p : ℝ → U) (hpAC : AbsolutelyContinuousOnInterval p 0 T) (hp : ↑↑(EulerTransverseMomentumRegularity.momentum T hT Q u) =ᵐ[EulerTimeLp.timeMeasure T] p) (hpder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt p (↑↑(EulerTransverseMomentumRegularity.momentumForcing T hT Q Q₁ H u f) t) t) : AbsolutelyContinuousOnInterval (velocityRepresentative T hT Q Q₁ c hc hQ u p) 0 T ∧ ↑↑(EulerTransverseCoordinateRegularity.coordinateDerivative T hT Q Q₁ c hc hQ u) =ᵐ[EulerTimeLp.timeMeasure T] velocityRepresentative T hT Q Q₁ c hc hQ u p ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (velocityRepresentative T hT Q Q₁ c hc hQ u p) (↑↑(coordinateSecondDerivative T hT Q Q₁ Q₂ c hc hQ H u f) t) t

Actual H¹ regularity of the coordinate velocity follows from actual H¹ momentum and the coefficient bounds.

theorem EulerTransverseStrongEquation.velocityRepresentative_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₁ 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) (hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (u f : ↥(EulerTimeLp.TimeLp T E)) (huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerTerminalTimePrimitive.realPrimitive T u ↑t) (hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t) (p : ℝ → U) (hpAC : AbsolutelyContinuousOnInterval p 0 T) (hp : ↑↑(EulerTransverseMomentumRegularity.momentum T hT Q u) =ᵐ[EulerTimeLp.timeMeasure T] p) (hpder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt p (↑↑(EulerTransverseMomentumRegularity.momentumForcing T hT Q Q₁ H u f) t) t) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, (EulerTransverseGramInverse.gram (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑(coordinateSecondDerivative T hT Q Q₁ Q₂ c hc hQ H u f) t) = (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑f t - 2 • (EulerVolterraConvolution.extendPath T hT Q₁ t) (↑↑(EulerTransverseCoordinateRegularity.coordinateDerivative T hT Q Q₁ c hc hQ u) t))

Differentiating the actual momentum identity gives exactly the projected strong equation; the sole potential cancellation is the prescribed frame ODE.

theorem EulerTransverseStrongEquation.exists_strong_of_weak_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₁ 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) (hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t) (hTpos : 0 < T) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (u f : ↥(EulerTimeLp.TimeLp T E)) (huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerTerminalTimePrimitive.realPrimitive T u ↑t) (hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t) (hweak : ∀ (v : ↥(EulerTimeLp.TimeLp T U)), (EulerTerminalTimePrimitive.initialTrace T hT) v = 0 → inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q u) v = -inner ℝ (EulerTransverseMomentumRegularity.momentumForcing T hT Q Q₁ H u f) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)) : ∃ (v : ℝ → U), AbsolutelyContinuousOnInterval (EulerTransverseCoordinateRegularity.coordinatePrimitive T hT Q c hc hQ u) 0 T ∧ AbsolutelyContinuousOnInterval v 0 T ∧ ↑↑(EulerTransverseCoordinateRegularity.coordinateDerivative T hT Q Q₁ c hc hQ u) =ᵐ[EulerTimeLp.timeMeasure T] v ∧ (∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (EulerTransverseCoordinateRegularity.coordinatePrimitive T hT Q c hc hQ u) (v t) t) ∧ (∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt v (↑↑(coordinateSecondDerivative T hT Q Q₁ Q₂ c hc hQ H u f) t) t) ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, (EulerTransverseGramInverse.gram (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑(coordinateSecondDerivative T hT Q Q₁ Q₂ c hc hQ H u f) t) = (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑f t - 2 • (EulerVolterraConvolution.extendPath T hT Q₁ t) (v t))

A general moving-frame weak solution has genuine H² coordinates and the literal strong projected evolution. The hypotheses concern only the original weak equation and the prescribed coefficient frame.

theorem EulerTransverseStrongEquation.transverseSolver_strong {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) (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) (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 = η) (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) (hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t) (f : ↥(EulerTimeLp.TimeLp T E)) : have u := ↑((EulerTransverseVariationalInverse.transverseSolver T hT m H K hK hH hsmall) f); ∃ (v : ℝ → U), AbsolutelyContinuousOnInterval (EulerTransverseCoordinateRegularity.coordinatePrimitive T hT Q c hc hQ u) 0 T ∧ AbsolutelyContinuousOnInterval v 0 T ∧ ↑↑(EulerTransverseCoordinateRegularity.coordinateDerivative T hT Q Q₁ c hc hQ u) =ᵐ[EulerTimeLp.timeMeasure T] v ∧ (∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (EulerTransverseCoordinateRegularity.coordinatePrimitive T hT Q c hc hQ u) (v t) t) ∧ (∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt v (↑↑(coordinateSecondDerivative T hT Q Q₁ Q₂ c hc hQ H u f) t) t) ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, (EulerTransverseGramInverse.gram (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑(coordinateSecondDerivative T hT Q Q₁ Q₂ c hc hQ H u f) t) = (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑f t - 2 • (EulerVolterraConvolution.extendPath T hT Q₁ t) (v t))

The actual coercively constructed transverse solver satisfies the strong projected equation (10), with genuine first and second time derivatives.