Fixed low-order constants are chosen before the stage and base scale. Their slack absorbs the universal good-time and first-packet ratios.

noncomputable def EulerPacketLowConstants.gradientConstant : ℝ

Gradient constant, given by 8*(1+initialCoefficientCost+firstRatio+goodRatio).

Equations

• EulerPacketLowConstants.gradientConstant = 8 * (1 + EulerBaseDatum.initialCoefficientCost + EulerPacketFirstLowBounds.firstRatio + EulerPacketGeometryLowBounds.goodRatio)

noncomputable def EulerPacketLowConstants.hessianConstant : ℝ

Hessian constant, given by 8*(1+initialCoefficientCost+2*gradientConstant*(firstRatio+goodRatio)).

Equations

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

noncomputable def EulerPacketLowConstants.frameConstant : ℝ

Frame constant, given by 1+gradientConstant+hessianConstant.

Equations

• EulerPacketLowConstants.frameConstant = 1 + EulerPacketLowConstants.gradientConstant + EulerPacketLowConstants.hessianConstant

theorem EulerPacketLowConstants.gradient_properties : 4 ≤ gradientConstant ∧ EulerBaseDatum.initialCoefficientCost + EulerPacketFirstLowBounds.firstRatio + 1 ≤ gradientConstant ∧ 4 * EulerPacketGeometryLowBounds.goodRatio ≤ gradientConstant

theorem EulerPacketLowConstants.gradient_nonneg : 0 ≤ gradientConstant

theorem EulerPacketLowConstants.hessian_properties : 4 ≤ hessianConstant ∧ EulerBaseDatum.initialCoefficientCost + 2 * EulerBaseDatum.initialCoefficientCost * EulerPacketFirstLowBounds.firstRatio + 1 ≤ hessianConstant ∧ 8 * gradientConstant * EulerPacketGeometryLowBounds.goodRatio ≤ hessianConstant

theorem EulerPacketLowConstants.hessian_nonneg : 0 ≤ hessianConstant

theorem EulerPacketLowConstants.frame_properties : 1 ≤ frameConstant ∧ gradientConstant ≤ frameConstant ∧ gradientConstant ^ 2 + hessianConstant ≤ frameConstant ^ 2

theorem EulerPacketLowConstants.initial_bounds (h e : ℝ) (hh : 1 ≤ h) (he : e ≤ 1) : EulerBaseDatum.initialCoefficientCost + h * EulerPacketFirstLowBounds.firstRatio + e ≤ gradientConstant * h ∧ EulerBaseDatum.initialCoefficientCost + 2 * EulerBaseDatum.initialCoefficientCost * (h * EulerPacketFirstLowBounds.firstRatio) + e ≤ hessianConstant * h