OAI/Probability/SKRatio/Certificates/CertifiedQuadrature.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Certificate.Box.absUpper line 12
  2. def OAI.SKRatio.Certificate.Box.widen line 13
  3. def OAI.SKRatio.Certificate.Box.contains line 15
  4. lemma OAI.SKRatio.Certificate.Box.mem_of_contains line 17
  5. lemma OAI.SKRatio.Certificate.Box.absUpper_nonneg line 23
  6. lemma OAI.SKRatio.Certificate.Box.abs_le_absUpper line 26
  7. lemma OAI.SKRatio.Certificate.Box.mem_widen line 31
  8. lemma OAI.SKRatio.Certificate.trapezoid_bound line 38
  9. def OAI.SKRatio.Certificate.Expr.cell line 64
  10. lemma OAI.SKRatio.Certificate.Expr.cell_sound line 72
  11. def OAI.SKRatio.Certificate.Expr.quad line 92
  12. lemma OAI.SKRatio.Certificate.Expr.quad_sound line 99
  13. def OAI.SKRatio.Certificate.Expr.check line 120
  14. lemma OAI.SKRatio.Certificate.Expr.check_sound line 125