OAI/Probability/SKRatio/Certificates/CertifiedInterpolation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Certificate.Box.posInv line 15
  2. def OAI.SKRatio.Certificate.Box.divPos line 16
  3. lemma OAI.SKRatio.Certificate.Box.mem_divPos line 17
  4. lemma OAI.SKRatio.Certificate.Box.lower line 22
  5. lemma OAI.SKRatio.Certificate.Box.upper line 24
  6. structure OAI.SKRatio.Certificate.Enclosures line 28
  7. structure OAI.SKRatio.Certificate.Valid line 38
  8. def OAI.SKRatio.Certificate.lBox line 48
  9. lemma OAI.SKRatio.Certificate.mem_lBox line 49
  10. def OAI.SKRatio.Certificate.coefficientBox line 54
  11. def OAI.SKRatio.Certificate.slackBox₀ line 58
  12. def OAI.SKRatio.Certificate.slackBox₁ line 62
  13. def OAI.SKRatio.Certificate.crossBox line 67
  14. lemma OAI.SKRatio.Certificate.coefficient_mem line 76
  15. lemma OAI.SKRatio.Certificate.slack₀_mem line 82
  16. lemma OAI.SKRatio.Certificate.slack₁_mem line 91
  17. lemma OAI.SKRatio.Certificate.cross_mem line 104
  18. def OAI.SKRatio.Certificate.interpolationCheck line 123
  19. lemma OAI.SKRatio.Certificate.interpolation_check_sound line 129
  20. lemma OAI.SKRatio.Certificate.certified_slacks line 145
  21. lemma OAI.SKRatio.Certificate.discriminant_of_slacks line 154