The actual fixed-coordinate Dirichlet inverse satisfies the strong equation

This version uses the range of the frame directly. It applies to supported spatial or cylinder L² spaces, where a pointwise transverse constraint must not be replaced by orthogonality to a single Hilbert-space vector.

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

The actual derivative of the physical displacement from the fixed inverse.

Equations

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

theorem EulerTransverseFixedStrong.physicalDerivative_range {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) (f : ↥(EulerTimeLp.TimeLp T E)) (t : ↑(Set.Icc 0 T)) : ∃ (v : U), (Q t) v = EulerTerminalTimePrimitive.realPrimitive T ((physicalDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) ↑t

theorem EulerTransverseFixedStrong.coordinateDerivative_eq {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) (f : ↥(EulerTimeLp.TimeLp T E)) : EulerTransverseCoordinateRegularity.coordinateDerivative T hT Q Q₁ c hc hQ ((physicalDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) = ↑((EulerTransverseFixedSpaceInverse.fixedFrameSolver T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f)

The existing coordinate derivative is exactly the solved fixed-space field.

theorem EulerTransverseFixedStrong.momentum_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)) (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) (f : ↥(EulerTimeLp.TimeLp T E)) (v : ↥(EulerTimeLp.TimeLp T U)) (hv : (EulerTerminalTimePrimitive.initialTrace T hT) v = 0) : inner ℝ (EulerTransverseMomentumRegularity.momentum T hT Q ((physicalDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f)) v = -inner ℝ (EulerTransverseMomentumRegularity.momentumForcing T hT Q Q₁ H ((physicalDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) f) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)

Actual product tests supply the weak momentum identity for this inverse.

theorem EulerTransverseFixedStrong.exists_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₁ : 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)) (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) (hTpos : 0 < T) (f : ↥(EulerTimeLp.TimeLp T E)) : have u := (physicalDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f; ∃ (v : ℝ → U), AbsolutelyContinuousOnInterval v 0 T ∧ ↑↑↑((EulerTransverseFixedSpaceInverse.fixedFrameSolver T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) =ᵐ[EulerTimeLp.timeMeasure T] v ∧ (∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt v (↑↑(EulerTransverseStrongEquation.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)) (↑↑(EulerTransverseStrongEquation.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 true H¹ coordinate velocity and equation (10) follow from the fixed coercive solve. There is no assumed strong solution or ambient normal.