OAI/Geometry/Convex/GeneralMahler/Middle/Poly.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Middle-width certificate uses second derivative envelope on the actual endpoint functional. Syntax shares proof of interval and profile estimates.

  1. inductive OAI.GeneralMahler.SCal.Mid.Op line 10
  2. def OAI.GeneralMahler.SCal.Mid.Op.eval line 20
  3. def OAI.GeneralMahler.SCal.Mid.Op.boxE line 26
  4. def OAI.GeneralMahler.SCal.Mid.Op.capE line 33
  5. lemma OAI.GeneralMahler.SCal.Mid.Op.bval line 40
  6. lemma OAI.GeneralMahler.SCal.Mid.Op.valGuard line 48
  7. def OAI.GeneralMahler.SCal.Mid.Op.q line 58

    Source comment

    endpoints stored 0,1; averages 2
    def q (v:Op):Op:=mul v v

    Mentions: OAI.GeneralMahler.SCal.Mid.Op

  8. def OAI.GeneralMahler.SCal.Mid.Op.ekp line 59
  9. def OAI.GeneralMahler.SCal.Mid.Op.gammaOp line 60
  10. def OAI.GeneralMahler.SCal.Mid.Op.ru2 line 66
  11. def OAI.GeneralMahler.SCal.Mid.Op.sm line 67
  12. def OAI.GeneralMahler.SCal.Mid.Op.dotOp line 68
  13. def OAI.GeneralMahler.SCal.Mid.Op.mb line 70
  14. def OAI.GeneralMahler.SCal.Mid.Op.bolt line 71
  15. def OAI.GeneralMahler.SCal.Mid.Op.E line 72
  16. def OAI.GeneralMahler.SCal.Mid.inp line 79

    Source comment

    choose s=g t profiles
    def inp (x y:ℝ):Fin 3→Ft→ℝ:=
…

    Mentions: OAI.GeneralMahler.SCal.Mid.Ft

  17. def OAI.GeneralMahler.SCal.Mid.Fval line 81
  18. def OAI.GeneralMahler.SCal.Mid.caps line 82
  19. def OAI.GeneralMahler.SCal.Mid.budgetCap line 83
  20. lemma OAI.GeneralMahler.SCal.Mid.gv2 line 84
  21. lemma OAI.GeneralMahler.SCal.Mid.Bcost line 92