ThresholdConstants.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.log_odds_le_two_log_half_inv line 10

Source documentation

The logarithmic simplification used in the threshold-width estimate.

theorem log_odds_le_two_log_half_inv (ε : ℝ) (hε : 0 < ε)
    (hεhalf : ε < (1 / 2 : ℝ)) :
    Real.log ((1 - ε) / ε) ≤ 2 * Real.log (1 / (2 * ε)) := by
…

theorem OAI.Problem313.threshold_log_conversion line 23

Source documentation

Multiplying the logarithmic estimate by a nonnegative constant.

theorem threshold_log_conversion (C ε w : ℝ) (hC : 0 ≤ C)
    (hε : 0 < ε) (hεhalf : ε < (1 / 2 : ℝ))
    (hw : w ≤ (2 * C) * Real.log ((1 - ε) / ε)) :
    w ≤ (4 * C) * Real.log (1 / (2 * ε)) := by
…

theorem OAI.Problem313.threshold_constant_conversion line 35

Source documentation

The numerical constants relating the variance and threshold-width bounds.

theorem threshold_constant_conversion (t ε w : ℝ)
    (hε : 0 < ε) (hεhalf : ε < (1 / 2 : ℝ))
    (hw : w ≤ ((2 * (2 : ℝ) ^ 17) / t ^ 2) *
      Real.log ((1 - ε) / ε)) :
    w ≤ ((2 : ℝ) ^ 19 / t ^ 2) * Real.log (1 / (2 * ε)) := by
…