Arithmetic #

Numerical estimates #

The square-root estimates and explicit constants in the final cost bounds.

theorem FD1D.sqrt_div_sqrt_six_le_four_div {x m : ℝ} (hm : 0 < m) (hx : x ≤ 96 / m ^ 2) :

theorem FD1D.stationary_sqrt_term_le {H m : ℝ} (hm : 0 < m) (hH : H ≤ 206 / (3 * m ^ 2)) :

√(H - 1 / m ^ 2) / √6 ≤ 4 / m

theorem FD1D.stationary_cost_le_six {a m H cell cost : ℝ} (ha : 0 ≤ a) (hm : 0 < m) (hcell : cell ≤ 2 * a / m) (hH : H ≤ 206 / (3 * m ^ 2)) (hcost : cost ≤ cell + a / √6 * √(H - 1 / m ^ 2)) :

cost ≤ 6 * a / m

Equation (3) plus the hazard bound implies the advertised stationary cost.

theorem FD1D.inv_horizon_le_inv_sq {T m : ℝ} (hm : 0 < m) (hT : m ^ 2 ≤ T) :

1 / T ≤ 1 / m ^ 2

theorem FD1D.transient_sqrt_term_le {H T m : ℝ} (hm : 0 < m) (hT : m ^ 2 ≤ T) (hH : H ≤ 206 / (3 * m ^ 2) + 1 / T) :

√(H - 1 / m ^ 2) / √6 ≤ 4 / m

theorem FD1D.transient_cost_le_six {a m T H cell cost : ℝ} (ha : 0 ≤ a) (hm : 0 < m) (hT : m ^ 2 ≤ T) (hcell : cell ≤ 2 * a / m) (hH : H ≤ 206 / (3 * m ^ 2) + 1 / T) (hcost : cost ≤ cell + a / √6 * √(H - 1 / m ^ 2)) :

cost ≤ 6 * a / m