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.bound_add {a a' b b' : ℝ} (ha : 0 ≤ a ∧ a ≤ a') (hb : 0 ≤ b ∧ b ≤ b') : 0 ≤ a + b ∧ a + b ≤ a' + b'

A nonnegative quantity bounded above passes its bound through a sum.

theorem EulerTransverseHistoryBounds.bound_mul {a a' b b' : ℝ} (ha : 0 ≤ a ∧ a ≤ a') (hb : 0 ≤ b ∧ b ≤ b') : 0 ≤ a * b ∧ a * b ≤ a' * b'

A nonnegative quantity bounded above passes its bound through a product.

theorem EulerTransverseHistoryBounds.bound_pow {a a' : ℝ} (ha : 0 ≤ a ∧ a ≤ a') (n : ℕ) : 0 ≤ a ^ n ∧ a ^ n ≤ a' ^ n

A nonnegative quantity bounded above passes its bound through a power.

theorem EulerTransverseHistoryBounds.bound_refl {a : ℝ} (ha : 0 ≤ a) : 0 ≤ a ∧ a ≤ a

theorem EulerTransverseHistoryBounds.slopeEnvelope_bound {Ti d a r Ti' d' a' r' : ℝ} (hTi : 0 ≤ Ti ∧ Ti ≤ Ti') (hd : 0 ≤ d ∧ d ≤ d') (ha : 0 ≤ a ∧ a ≤ a') (hr : 0 ≤ r ∧ r ≤ r') : 0 ≤ slopeEnvelope Ti d a r ∧ slopeEnvelope Ti d a r ≤ slopeEnvelope Ti' d' a' r'

theorem EulerTransverseHistoryBounds.endpointDifferenceCost_bound {d i a x y d' i' a' x' y' : ℝ} (hd : 0 ≤ d ∧ d ≤ d') (hi : 0 ≤ i ∧ i ≤ i') (ha : 0 ≤ a ∧ a ≤ a') (hx : 0 ≤ x ∧ x ≤ x') (hy : 0 ≤ y ∧ y ≤ y') : 0 ≤ EulerTransverseEndpointDifference.endpointDifferenceCost d i a x y ∧ EulerTransverseEndpointDifference.endpointDifferenceCost d i a x y ≤ EulerTransverseEndpointDifference.endpointDifferenceCost d' i' a' x' y'

theorem EulerTransverseHistoryBounds.slopeDifferenceEnvelope_bound {Ti d a r x y Ti' d' a' r' x' y' : ℝ} (hTi : 0 ≤ Ti ∧ Ti ≤ Ti') (hd : 0 ≤ d ∧ d ≤ d') (ha : 0 ≤ a ∧ a ≤ a') (hr : 0 ≤ r ∧ r ≤ r') (hx : 0 ≤ x ∧ x ≤ x') (hy : 0 ≤ y ∧ y ≤ y') : 0 ≤ slopeDifferenceEnvelope Ti d a r x y ∧ slopeDifferenceEnvelope Ti d a r x y ≤ slopeDifferenceEnvelope Ti' d' a' r' x' y'

theorem EulerTransverseHistoryBounds.generatorDifferenceEnvelope_bound {ci q q1 x y ci' q' q1' x' y' : ℝ} (hci : 0 ≤ ci ∧ ci ≤ ci') (hq : 0 ≤ q ∧ q ≤ q') (hq1 : 0 ≤ q1 ∧ q1 ≤ q1') (hx : 0 ≤ x ∧ x ≤ x') (hy : 0 ≤ y ∧ y ≤ y') : 0 ≤ generatorDifferenceEnvelope ci q q1 x y ∧ generatorDifferenceEnvelope ci q q1 x y ≤ generatorDifferenceEnvelope ci' q' q1' x' y'

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

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.