OAI/Probability/SKRatio/Certificates/FixedExp.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatio.Certificate.Fixed.S line 9
2. structure OAI.SKRatio.Certificate.Fixed.I line 10
3. def OAI.SKRatio.Certificate.Fixed.Mem line 15
4. def OAI.SKRatio.Certificate.Fixed.round line 16
5. def OAI.SKRatio.Certificate.Fixed.sq line 17
6. def OAI.SKRatio.Certificate.Fixed.iter line 18
7. def OAI.SKRatio.Certificate.Fixed.expBounds line 21
8. lemma OAI.SKRatio.Certificate.Fixed.S_pos line 24
9. lemma OAI.SKRatio.Certificate.Fixed.mem_round line 25
10. lemma OAI.SKRatio.Certificate.Fixed.mem_sq line 32
11. lemma OAI.SKRatio.Certificate.Fixed.mem_iter line 56
12. lemma OAI.SKRatio.Certificate.Fixed.mem_expBounds line 64