Reusable bounds for the actual parameters entering the canonical correction. They all use the same fixed polynomial envelope.
theorem
EulerPacketInitializedCost.actual_parameters
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
(W H0 : ℝ)
(hδ : 0 < δ)
(H : EulerPacketRadiusPolynomial.RadiusPrimitives LM L NB BC δ ξ W)
(hH0 : H0 ≤ W)
:
1 ≤ envelope W ∧ EulerPacketTerminalDatum.initializedRadius 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
EulerPacketRadiusPolynomial.RadiusPrimitives.mono
{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τ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O}
{LM : EulerMeanPacketProvider.Budget M 6 Rm}
{L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
{NB : EulerTransversePacketJoin.NormalBudget D 6 L.R}
{BC : EulerPacketCylinderField.CoefficientBudget C}
{δ : ℝ}
{ξ : U}
{X Y : ℝ}
(H : RadiusPrimitives LM L NB BC δ ξ X)
(hXY : X ≤ Y)
:
RadiusPrimitives LM L NB BC δ ξ Y