LocalFailureNumerics.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LeanBlast.SecondKahnKalai.two_lt_exp_one line 14
theorem OAI.LeanBlast.SecondKahnKalai.exp_one_lt_three line 16
theorem OAI.LeanBlast.SecondKahnKalai.predecessor_power_lt_one line 20
Source documentation
The strict numerical estimate used to rule out large maximizing predecessors in the graph hierarchy.
```
theorem predecessor_power_lt_one {r : ℕ} (hr : 1 ≤ r) :
    2 * (17 * Real.exp 1 / 128) ^ r < 1 := by
…
```
theorem OAI.LeanBlast.SecondKahnKalai.exp_neg_fifty_lt_one line 29
theorem OAI.LeanBlast.SecondKahnKalai.one_add_le_exp_one_of_le_exp_neg_fifty line 32
theorem OAI.LeanBlast.SecondKahnKalai.one_add_pow_le_exp_nat line 36
theorem OAI.LeanBlast.SecondKahnKalai.two_pow_le_exp_nat line 44

theorem OAI.LeanBlast.SecondKahnKalai.large_intersection_power_le line 50

Source documentation

A term beyond half the capacity has the required exponential decay.

theorem large_intersection_power_le {m r : ℕ} {q : ℝ}
    (hq0 : 0 ≤ q) (hq : q ≤ Real.exp (-50)) (hr : m < 2 * r) :
    q ^ r ≤ Real.exp (-25 * (m : ℝ)) := by
…

def OAI.LeanBlast.SecondKahnKalai.largeIntersectionTail line 60
Source documentation
The finite binomial upper tail used by the resampling argument.
```
def largeIntersectionTail (m : ℕ) (q : ℝ) : ℝ :=
…
```
theorem OAI.LeanBlast.SecondKahnKalai.largeIntersectionTail_le line 63
theorem OAI.LeanBlast.SecondKahnKalai.local_failure_exponential_combine line 79