Both nonlinear-profile and exact-correction coefficient budgets are derived from the original joined-source coefficient bounds.
noncomputable def
EulerPacketCylinderField.joinedCoefficientBudget
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
{R : ℝ}
(NB : EulerTransversePacketJoin.NormalBudget D 6 R)
:
CoefficientBudget (joinedSourceCoefficientData P M D τ hτ hτT B hTime)
Joined coefficient budget as an element of CoefficientBudget (joinedSourceCoefficientData P M D τ hτ hτT B hTime).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransversePacketJoin.Budget.correctionCoefficients
{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τ ⋯)}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(NB : NormalBudget D 6 L.R)
(P : ℝ)
[Fact (0 < P)]
:
No additional coefficient-bound hypothesis is needed by correction: the source frame, frame derivative and inverse bounds already suffice.
Equations
- L.correctionCoefficients NB P = EulerPacketCorrectionCoefficients.correctionCoefficientBudget D P (max L.Rc NB.Rc) L.C₀ L.C₁ NB.C ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯