A fixed polynomial upper bound for the history's computed sensitivity. The time reciprocal and inverse Gram bound are independent scalar inputs; no operator or solution norm occurs in the resulting envelope.

def EulerTransverseHistoryBounds.slopeEnvelope (Ti d a r : ℝ) : ℝ

Slope envelope, given by r*(1+d^2*(2*r^2)*a)*(2*Ti*d).

Equations

• EulerTransverseHistoryBounds.slopeEnvelope Ti d a r = r * (1 + d ^ 2 * (2 * r ^ 2) * a) * (2 * Ti * d)

def EulerTransverseHistoryBounds.slopeDifferenceEnvelope (Ti d a r x y : ℝ) : ℝ

Slope difference envelope, given by r*(2*Ti*endpointDifferenceCost d (2*r^2) a x y+x*slopeEnvelope Ti d a r).

Equations

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

def EulerTransverseHistoryBounds.generatorDifferenceEnvelope (ci q q1 x y : ℝ) : ℝ

Generator difference envelope, given by (4*ci^2*q^2*q1+2*ci*q1)*x+2*ci*q*y.

Equations

• EulerTransverseHistoryBounds.generatorDifferenceEnvelope ci q q1 x y = (4 * ci ^ 2 * q ^ 2 * q1 + 2 * ci * q1) * x + 2 * ci * q * y

def EulerTransverseHistoryBounds.differenceEnvelope (Ti ci q q1 d a r x y z : ℝ) : ℝ

Difference envelope as an element of ℝ.

Equations

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

theorem EulerTransverseHistoryBounds.differenceEnvelope_nonneg (Ti ci q q1 d a r x y z : ℝ) (hTi : 0 ≤ Ti) (hci : 0 ≤ ci) (hq : 0 ≤ q) (hq1 : 0 ≤ q1) (hd : 0 ≤ d) (ha : 0 ≤ a) (hr : 0 ≤ r) (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) : 0 ≤ differenceEnvelope Ti ci q q1 d a r x y z

theorem EulerTransverseHistoryBounds.historyDifferenceCost_le_envelope (T c Ti ci q q1 d a r x y z : ℝ) (hT : 0 < T) (hT1 : T ≤ 1) (hTi : T⁻¹ ≤ Ti) (hc : 0 < c) (hci : c⁻¹ ≤ ci) (hq : 0 ≤ q) (hq1 : 0 ≤ q1) (hd : 0 ≤ d) (ha : 0 ≤ a) (hr : 0 ≤ r) (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) : historyDifferenceCost T c q q1 d a r x y z ≤ differenceEnvelope Ti ci q q1 d a r x y z

theorem EulerTransverseHistoryBounds.differenceEnvelope_mono {Ti ci q q1 d a r x y z Ti' ci' q' q1' d' a' r' x' y' z' : ℝ} (hTi : 0 ≤ Ti) (hci : 0 ≤ ci) (hq : 0 ≤ q) (hq1 : 0 ≤ q1) (hd : 0 ≤ d) (ha : 0 ≤ a) (hr : 0 ≤ r) (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) (hTi' : Ti ≤ Ti') (hci' : ci ≤ ci') (hq' : q ≤ q') (hq1' : q1 ≤ q1') (hd' : d ≤ d') (ha' : a ≤ a') (hr' : r ≤ r') (hx' : x ≤ x') (hy' : y ≤ y') (hz' : z ≤ z') : differenceEnvelope Ti ci q q1 d a r x y z ≤ differenceEnvelope Ti' ci' q' q1' d' a' r' x' y' z'

def EulerTransverseHistoryBounds.parentDifferenceEnvelope (Ti C C1 CH R : ℝ) : ℝ

Parent difference envelope, given by differenceEnvelope Ti (gramInverseEnvelope C) C C1 (C1+C) (1+CH) (transportEnvelope C C1) (C*R) (C1*R) (CH*R).

Equations

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