The actual forward source coefficients supply both the nonlinear-profile budget and the all-order correction coefficient budget.

noncomputable def EulerPacketCylinderField.forwardCoefficientBudget (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) {R : ℝ} (NB : EulerTransversePacketJoin.NormalBudget D 6 R) : CoefficientBudget (sourceCoefficientData P M D (EulerTransversePacketProvider.InitialData.zero P D) hTime)

Forward coefficient budget, given by sourceCoefficientBudget P M D (InitialData.zero P D) hTime NB.Rc NB.C NB.Rc_nonneg NB.C_nonneg NB.inverse_bound NB.strain_bound.

Equations

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

noncomputable def EulerTransversePacketForward.Budget.correctionCoefficients {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (L : Budget D (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (P : ℝ) [Fact (0 < P)] : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P

Correction coefficients, constructed using correctionCoefficientBudget.

Equations

• L.correctionCoefficients NB P = EulerPacketCorrectionCoefficients.correctionCoefficientBudget D P (max L.Rc NB.Rc) L.C₀ L.C₁ NB.C ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯