OAI/Combinatorics/CliqueFree/Numerical.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CliqueFreeIndependence.Numerical.log_bounds line 18
2. lemma OAI.CliqueFreeIndependence.Numerical.pow_six_le_exp line 34
3. lemma OAI.CliqueFreeIndependence.Numerical.exp_neg_le_inv_pow_seven line 43
4. def OAI.CliqueFreeIndependence.Numerical.threshold line 53
5. lemma OAI.CliqueFreeIndependence.Numerical.threshold_pos line 55
6. lemma OAI.CliqueFreeIndependence.Numerical.growth_factor_le line 58
7. lemma OAI.CliqueFreeIndependence.Numerical.leakage_factor line 77
8. lemma OAI.CliqueFreeIndependence.Numerical.ceil_bounds line 82
9. def OAI.CliqueFreeIndependence.Numerical.lossRatio line 97
10. def OAI.CliqueFreeIndependence.Numerical.scale line 99
11. lemma OAI.CliqueFreeIndependence.Numerical.scale_ge line 103
12. lemma OAI.CliqueFreeIndependence.Numerical.scale_ge_add line 111
13. lemma OAI.CliqueFreeIndependence.Numerical.lossRatio_nonneg line 119
14. lemma OAI.CliqueFreeIndependence.Numerical.lossRatio_square line 122
15. lemma OAI.CliqueFreeIndependence.Numerical.lossRatio_scale line 143
16. lemma OAI.CliqueFreeIndependence.Numerical.inv_scale line 154
17. lemma OAI.CliqueFreeIndependence.Numerical.exists_iteration_threshold line 170
18. lemma OAI.CliqueFreeIndependence.Numerical.recurrence_bound line 180