One fixed polynomial controls the complete history sensitivity envelope for all parent label constants and reciprocal time bounds.

noncomputable def EulerParentHistoryCost.labelHistoryEnvelope (K Ti : ℝ) : ℝ

Label history envelope, constructed using parentDifferenceEnvelope.

Equations

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

noncomputable def EulerParentHistoryCost.labelHistoryPolynomial : Polynomial ℝ

Label history polynomial as an element of Polynomial ℝ.

Equations

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

theorem EulerParentHistoryCost.labelHistoryPolynomial_eval (P : ℝ) : Polynomial.eval P labelHistoryPolynomial = EulerTransverseHistoryBounds.parentDifferenceEnvelope P (EulerPacketParentLabelBounds.frameAmplitude P) (EulerPacketParentLabelBounds.gradientAmplitude P) (27 * EulerPacketParentLabelBounds.frameAmplitude P ^ 2 * EulerPacketParentLabelBounds.gradientAmplitude P) (1024 + 4 * P)

noncomputable def EulerParentHistoryCost.labelHistoryConstant : ℝ

Label history constant, given by coefficientCost labelHistoryPolynomial.

Equations

• EulerParentHistoryCost.labelHistoryConstant = EulerPolynomialCost.coefficientCost EulerParentHistoryCost.labelHistoryPolynomial

noncomputable def EulerParentHistoryCost.labelHistoryPower : ℕ

Label history power, given by labelHistoryPolynomial.natDegree.

Equations

• EulerParentHistoryCost.labelHistoryPower = EulerParentHistoryCost.labelHistoryPolynomial.natDegree

theorem EulerParentHistoryCost.labelHistoryConstant_pos : 0 < labelHistoryConstant

theorem EulerParentHistoryCost.labelHistoryEnvelope_power (K Ti : ℝ) (hK : 0 ≤ K) (hTi : 0 ≤ Ti) : labelHistoryEnvelope K Ti ≤ labelHistoryConstant * (1 + K + Ti) ^ labelHistoryPower