OAI/Probability/SKRatio/Certificates/CertifiedInterval.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Certificate.scale line 10
  2. def OAI.SKRatio.Certificate.down line 12
  3. def OAI.SKRatio.Certificate.up line 13
  4. lemma OAI.SKRatio.Certificate.down_le line 15
  5. lemma OAI.SKRatio.Certificate.le_up line 21
  6. structure OAI.SKRatio.Certificate.Box line 27
  7. def OAI.SKRatio.Certificate.Box.Mem line 34
  8. instance OAI.SKRatio.Certificate.Box.(instance at line 35) line 35
  9. def OAI.SKRatio.Certificate.Box.rat line 37
  10. def OAI.SKRatio.Certificate.Box.round line 38
  11. def OAI.SKRatio.Certificate.Box.add line 39
  12. def OAI.SKRatio.Certificate.Box.neg line 40
  13. def OAI.SKRatio.Certificate.Box.sub line 41
  14. def OAI.SKRatio.Certificate.Box.mul line 42
  15. def OAI.SKRatio.Certificate.Box.inv line 45
  16. def OAI.SKRatio.Certificate.Box.sq line 47
  17. def OAI.SKRatio.Certificate.Box.squareIter line 51
  18. def OAI.SKRatio.Certificate.Box.exp line 55
  19. lemma OAI.SKRatio.Certificate.Box.mem_rat line 61
  20. lemma OAI.SKRatio.Certificate.Box.mem_round line 62
  21. lemma OAI.SKRatio.Certificate.Box.mem_add line 64
  22. lemma OAI.SKRatio.Certificate.Box.mem_neg line 68
  23. lemma OAI.SKRatio.Certificate.Box.mem_sub line 72
  24. lemma OAI.SKRatio.Certificate.Box.four_products line 75
  25. lemma OAI.SKRatio.Certificate.Box.mem_mul line 114
  26. lemma OAI.SKRatio.Certificate.Box.mem_inv line 119
  27. lemma OAI.SKRatio.Certificate.Box.mem_sq line 130
  28. lemma OAI.SKRatio.Certificate.Box.mem_squareIter line 146
  29. lemma OAI.SKRatio.Certificate.Box.mem_exp line 153