Literal source operators with the complete positive-history-time high inverse.
noncomputable def
EulerPacketCylinderField.joinedSourceOperators
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
:
Joined source operators, bundling interval, period, inverseFrame, strain and the
required compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.joinedSourceCoefficientData
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(hT : M.T = D.T)
:
CoefficientData P M.T (joinedSourceOperators P M D τ hτ hτT B)
Joined source coefficient data, bundling period_eq, interval_eq, inverse, strain and
the required compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.