OAI/Probability/SKRatio/Certificates/CertifiedConstants.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Certificate.sqrt_densityFactor_bound line 11
2. def OAI.SKRatio.Certificate.X0 line 25
3. def OAI.SKRatio.Certificate.X1 line 35
4. def OAI.SKRatio.Certificate.X2 line 45
5. def OAI.SKRatio.Certificate.X3 line 55
6. def OAI.SKRatio.Certificate.X4 line 65
7. lemma OAI.SKRatio.Certificate.density0 line 75
8. lemma OAI.SKRatio.Certificate.check0 line 77
9. lemma OAI.SKRatio.Certificate.density1 line 79
10. lemma OAI.SKRatio.Certificate.check1 line 81
11. lemma OAI.SKRatio.Certificate.density2 line 83
12. lemma OAI.SKRatio.Certificate.check2 line 85
13. lemma OAI.SKRatio.Certificate.density3 line 87
14. lemma OAI.SKRatio.Certificate.check3 line 89