Actual momentum regularity of the transverse variational inverse #
The admissible tests are constructed by differentiating Q(t) Jv(t) with the
proved time-H¹ product rule. The weak equation then forces Q* η_t to have an
absolutely continuous representative. No momentum equation or second derivative
of the solved displacement is included in the assumptions.
noncomputable def
EulerTransverseMomentumRegularity.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 : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(u : ↥(EulerTimeLp.TimeLp T E))
:
↥(EulerTimeLp.TimeLp T U)
The literal transverse momentum as an actual L² field.
Equations
- EulerTransverseMomentumRegularity.momentum T hT Q u = (ContinuousLinearMap.adjoint (EulerTimeLp.timeMultiplier T hT Q)) u
Instances For
noncomputable def
EulerTransverseMomentumRegularity.momentumForcing
{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 f : ↥(EulerTimeLp.TimeLp T E))
:
↥(EulerTimeLp.TimeLp T U)
The forcing for the momentum derivative, before using the frame ODE.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransverseMomentumRegularity.momentum_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 : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(u : ↥(EulerTimeLp.TimeLp T E))
:
↑↑(momentum T hT Q u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) =>
(ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑u t)
The momentum field is pointwise Q(t)* u(t) almost everywhere.
theorem
EulerTransverseMomentumRegularity.momentumForcing_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 f : ↥(EulerTimeLp.TimeLp T E))
:
↑↑(momentumForcing T hT Q Q₁ H u f) =ᵐ[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) (EulerTerminalTimePrimitive.realPrimitive T u t)) + (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑f t)
The momentum forcing has its literal pointwise expression.
theorem
EulerTransverseMomentumRegularity.productDerivative_mem_transverse
{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))
(hQ : ∀ (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)
(v : ↥(EulerTimeLp.TimeLp T U))
(hv : (EulerTerminalTimePrimitive.initialTrace T hT) v = 0)
:
Every zero-endpoint coordinate test gives a genuine admissible physical test.
theorem
EulerTransverseMomentumRegularity.momentum_weak_of_product_tests
{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))
(hQ : ∀ (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))
(v : ↥(EulerTimeLp.TimeLp T U))
(htest :
inner ℝ u ((EulerTimeH1OperatorProduct.productDerivative T hT Q Q₁) v) - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) u))
((EulerTerminalTimePrimitive.primitiveTimeLp T hT)
((EulerTimeH1OperatorProduct.productDerivative T hT Q Q₁) v)) = -inner ℝ f
((EulerTerminalTimePrimitive.primitiveTimeLp T hT)
((EulerTimeH1OperatorProduct.productDerivative T hT Q Q₁) v)))
:
inner ℝ (momentum T hT Q u) v = -inner ℝ (momentumForcing T hT Q Q₁ H u f) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)
Generic momentum extraction from the actual product-test identity. This also applies to closed spatial Hilbert constraints, such as the solenoidal mean space.
theorem
EulerTransverseMomentumRegularity.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))
(hQ : ∀ (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)
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(u : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m))
(f : ↥(EulerTimeLp.TimeLp T E))
(hu :
∀ (v : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)),
inner ℝ ↑u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((EulerTransverseVariationalInverse.transversePrimitive T hT m) u))
((EulerTransverseVariationalInverse.transversePrimitive T hT m) v) = -inner ℝ f ((EulerTransverseVariationalInverse.transversePrimitive T hT m) v))
(v : ↥(EulerTimeLp.TimeLp T U))
(hv : (EulerTerminalTimePrimitive.initialTrace T hT) v = 0)
:
inner ℝ (momentum T hT Q ↑u) v = -inner ℝ (momentumForcing T hT Q Q₁ H (↑u) f) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)
The variational equation determines the weak derivative of actual momentum.
theorem
EulerTransverseMomentumRegularity.transverseSolver_momentum_ac
{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))
(hTpos : 0 < T)
(hQ : ∀ (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)
(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))
:
have u := ↑((EulerTransverseVariationalInverse.transverseSolver T hT m H K hK hH hsmall) f);
∃ (p : ℝ → U),
AbsolutelyContinuousOnInterval p 0 T ∧ ↑↑(momentum T hT Q u) =ᵐ[EulerTimeLp.timeMeasure T] p ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt p (↑↑(momentumForcing T hT Q Q₁ H u f) t) t
The actual solved transverse momentum has an AC representative and the prescribed genuine a.e. derivative. This is a regularity conclusion of the solve.