A fixed polynomial bounds all five costs for the literal canonical initialized packet radius. No arbitrary radius witness is used.

noncomputable def EulerPacketInitializedCost.envelope (W : ℝ) : ℝ

Envelope, given by 1+W+EulerPacketRadiusPolynomial.radiusEnvelope W + EulerPacketCorrectionPrimitive.primitiveEnvelope period W.

Equations

• EulerPacketInitializedCost.envelope W = 1 + W + EulerPacketRadiusPolynomial.radiusEnvelope W + EulerPacketCorrectionPrimitive.primitiveEnvelope EulerPacketTerminalDatum.period W

noncomputable def EulerPacketInitializedCost.polynomial : Polynomial ℝ

Polynomial, constructed using Polynomial.C.

noncomputable def EulerPacketInitializedCost.uniformConstant : ℝ

Uniform constant, given by coefficientCost polynomial.

Equations

• EulerPacketInitializedCost.uniformConstant = EulerPolynomialCost.coefficientCost EulerPacketInitializedCost.polynomial

noncomputable def EulerPacketInitializedCost.uniformPower : ℕ

Uniform power, given by polynomial.natDegree.

Equations

• EulerPacketInitializedCost.uniformPower = EulerPacketInitializedCost.polynomial.natDegree

theorem EulerPacketInitializedCost.uniformConstant_pos : 0 < uniformConstant

theorem EulerPacketInitializedCost.polynomial_eval (W : ℝ) : Polynomial.eval W polynomial = EulerPacketFiveCost.costConstant EulerPacketTerminalDatum.period * envelope W ^ EulerPacketFiveCost.costPower EulerPacketTerminalDatum.period

theorem EulerPacketInitializedCost.envelope_bound (W : ℝ) (hW : 1 ≤ W) : EulerPacketFiveCost.costConstant EulerPacketTerminalDatum.period * envelope W ^ EulerPacketFiveCost.costPower EulerPacketTerminalDatum.period ≤ uniformConstant * W ^ uniformPower

theorem EulerPacketInitializedCost.initialized_five_costs_bound {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 : 0 ≤ H0) (hHW : H0 ≤ W) : have R := EulerPacketTerminalDatum.initializedRadius 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