Coefficient identities in the strong transverse equation #
The only cancellation used here is the source frame equation Q_tt = -H Q.
The time derivatives of the Gram and mixed coefficients are genuine derivatives
of the prescribed coefficient paths.
noncomputable def
EulerTransverseStrongAlgebra.mixedPath
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
:
The mixed coefficient Q* Q_t in the transverse momentum.
Equations
- EulerTransverseStrongAlgebra.mixedPath T Q Q₁ = { toFun := fun (t : ↑(Set.Icc 0 T)) => ContinuousLinearMap.adjoint (Q t) ∘SL Q₁ t, continuous_toFun := ⋯ }
Instances For
noncomputable def
EulerTransverseStrongAlgebra.mixedDerivativePath
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(Q Q₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
:
The actual product-rule derivative Q_t* Q_t + Q* Q_tt.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransverseStrongAlgebra.gramPath_hasDerivWithinAt
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hT : 0 ≤ T)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerTransverseGramPath.gramPath T Q))
((EulerTransverseGramPath.gramDerivativePath T Q Q₁) t) (Set.Icc 0 T) ↑t
The actual Gram derivative on the time interval.
theorem
EulerTransverseStrongAlgebra.mixedPath_hasDerivWithinAt
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(Q Q₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hT : 0 ≤ T)
(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)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (mixedPath T Q Q₁)) ((mixedDerivativePath T Q Q₁ Q₂) t)
(Set.Icc 0 T) ↑t
The actual mixed-coefficient derivative on the time interval.
theorem
EulerTransverseStrongAlgebra.inverse_momentum_identity
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(Q Q₁ : U →L[ℝ] E)
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (x : U), c * ‖x‖ ^ 2 ≤ ‖Q x‖ ^ 2)
(ξ v : U)
(u : E)
(hu : u = Q₁ ξ + Q v)
:
(EulerTransverseGramInverse.gramInverse Q c hc hQ)
((ContinuousLinearMap.adjoint Q) u - (ContinuousLinearMap.adjoint Q) (Q₁ ξ)) = v
The genuine Gram inverse recovers the coordinate velocity from momentum.
theorem
EulerTransverseStrongAlgebra.projected_equation_of_momentum_balance
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(Q Q₁ Q₂ : U →L[ℝ] E)
(H : E →L[ℝ] E)
(ξ v a : U)
(u f : E)
(hu : u = Q₁ ξ + Q v)
(hframe : Q₂ = -H ∘SL Q)
(hbalance :
(ContinuousLinearMap.adjoint Q₁) u - (ContinuousLinearMap.adjoint Q) (H (Q ξ)) + (ContinuousLinearMap.adjoint Q) f = (ContinuousLinearMap.adjoint Q₁ ∘SL Q + ContinuousLinearMap.adjoint Q ∘SL Q₁) v + (EulerTransverseGramInverse.gram Q) a + (ContinuousLinearMap.adjoint Q₁ ∘SL Q₁ + ContinuousLinearMap.adjoint Q ∘SL Q₂) ξ + (ContinuousLinearMap.adjoint Q) (Q₁ v))
:
The frame equation cancels the potential term and gives exactly the projected coordinate equation (10).