OAI/Geometry/Convex/GeneralMahler/Scalar/LapBox.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

§07 interval enclosures for the Ymk via Taylor and CF.

  1. def OAI.GeneralMahler.SCal.phi0B line 10
  2. def OAI.GeneralMahler.SCal.cxB line 11
  3. def OAI.GeneralMahler.SCal.phiB line 12
  4. lemma OAI.GeneralMahler.SCal.mphi0 line 13
  5. lemma OAI.GeneralMahler.SCal.mcx line 16
  6. lemma OAI.GeneralMahler.SCal.mphi line 17
  7. def OAI.GeneralMahler.SCal.pSeries line 21
  8. def OAI.GeneralMahler.SCal.pTaylor line 25
  9. lemma OAI.GeneralMahler.SCal.mpSeries line 29
  10. lemma OAI.GeneralMahler.SCal.p_int_beta line 41
  11. lemma OAI.GeneralMahler.SCal.pT_bound line 57
  12. lemma OAI.GeneralMahler.SCal.mpTaylor line 94
  13. def OAI.GeneralMahler.SCal.cEncl line 105
  14. lemma OAI.GeneralMahler.SCal.mcEncl line 108
  15. def OAI.GeneralMahler.SCal.forward line 121
  16. lemma OAI.GeneralMahler.SCal.mforward line 125
  17. def OAI.GeneralMahler.SCal.prodCF line 134
  18. lemma OAI.GeneralMahler.SCal.mprodCF line 137
  19. def OAI.GeneralMahler.SCal.ymBox line 149
  20. lemma OAI.GeneralMahler.SCal.myBox line 153