The direct-forward branch uses the identical fixed polynomial cost envelope as the positive-history branch.
theorem
EulerPacketInitializedCost.forward_actual_parameters
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
(W H0 : ℝ)
(hδ : 0 < δ)
(H : EulerPacketForwardRadius.RadiusPrimitives L LM NB BC δ ξ W)
(hH0 : H0 ≤ W)
:
1 ≤ envelope W ∧ EulerPacketTerminalDatum.forwardInitializedRadius LM L NB BC δ ξ ≤ envelope W ∧ H0 ≤ envelope W ∧ BC.multiplierCost ≤ envelope W ∧ EulerPacketCorrectionPrimitive.CorrectionBounds D EulerPacketTerminalDatum.period
(L.correctionCoefficients NB EulerPacketTerminalDatum.period) (envelope W)
theorem
EulerPacketInitializedCost.forward_five_costs_bound
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
(W H0 : ℝ)
(hδ : 0 < δ)
(H : EulerPacketForwardRadius.RadiusPrimitives L LM NB BC δ ξ W)
(hH0 : 0 ≤ H0)
(hHW : H0 ≤ W)
:
have R := EulerPacketTerminalDatum.forwardInitializedRadius LM L NB BC δ ξ;
have Kc := L.correctionCoefficients NB EulerPacketTerminalDatum.period;
EulerPacketCoarseMajorant.tailPolynomialConstant R H0 BC.termCost ≤ uniformConstant * W ^ uniformPower ∧ BC.multiplierCost ≤ uniformConstant * W ^ uniformPower ∧ 12 * EulerPacketCorrectionConstants.growth D EulerPacketTerminalDatum.period Kc R H0 BC.multiplierCost * D.T ≤ uniformConstant * W ^ uniformPower ∧ 8 * EulerPacketCorrectionConstants.growth D EulerPacketTerminalDatum.period Kc R H0 BC.multiplierCost * D.T * EulerPacketCorrectionConstants.drift R H0 BC.multiplierCost / EulerPacketCorrectionScalar.initialRadius R Kc.M Kc.Rc ≤ uniformConstant * W ^ uniformPower ∧ 8 * EulerPacketCorrectionConstants.growth D EulerPacketTerminalDatum.period Kc R H0 BC.multiplierCost * D.T / EulerPacketCorrectionScalar.initialRadius R Kc.M Kc.Rc ≤ uniformConstant * W ^ uniformPower