The actual zeroth-order history costs are bounded by fixed scalar polynomials in the parent coefficient bounds and reciprocal horizon.

noncomputable def EulerTransverseHistoryBounds.scalarTransport (T c q q1 : ℝ) : ℝ

Scalar transport, given by 1+((2*(c⁻¹)^2*q^2*q1+c⁻¹*q1)*T+c⁻¹*q).

Equations

• EulerTransverseHistoryBounds.scalarTransport T c q q1 = 1 + ((2 * c⁻¹ ^ 2 * q ^ 2 * q1 + c⁻¹ * q1) * T + c⁻¹ * q)

theorem EulerTransverseHistoryBounds.historyDifferenceCost_le_parentEnvelope (T c q q1 h Ti C C1 CH R : ℝ) (hT : 0 < T) (hT1 : T ≤ 1) (hTi : T⁻¹ ≤ Ti) (hc : 0 < c) (hci : c⁻¹ ≤ EulerPacketParentMeanCoercivity.gramInverseEnvelope C) (hq0 : 0 ≤ q) (hq10 : 0 ≤ q1) (hh0 : 0 ≤ h) (hC : 0 ≤ C) (hC1 : 0 ≤ C1) (hCH : 0 ≤ CH) (hR : 0 ≤ R) (hq : q ≤ C) (hq1 : q1 ≤ C1) (hh : h ≤ CH) : historyDifferenceCost T c q q1 (T * q1 + q) (1 + T ^ 2 * h) (scalarTransport T c q q1) (C * R) (C1 * R) (CH * R) ≤ parentDifferenceEnvelope Ti C C1 CH R

theorem EulerTransverseHistoryBounds.parentDifferenceEnvelope_mono {Ti C C1 CH R Ti' C' C1' CH' R' : ℝ} (hTi : 0 ≤ Ti) (hC : 0 ≤ C) (hC1 : 0 ≤ C1) (hCH : 0 ≤ CH) (hR : 0 ≤ R) (hTi' : Ti ≤ Ti') (hC' : C ≤ C') (hC1' : C1 ≤ C1') (hCH' : CH ≤ CH') (hR' : R ≤ R') : parentDifferenceEnvelope Ti C C1 CH R ≤ parentDifferenceEnvelope Ti' C' C1' CH' R'