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

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Interval on t; second derivative majorants.

  1. structure OAI.GeneralMahler.SCal.Mid.Cap line 12
  2. def OAI.GeneralMahler.SCal.Mid.Cap.plus line 17
  3. def OAI.GeneralMahler.SCal.Mid.Cap.times line 18
  4. def OAI.GeneralMahler.SCal.Mid.Cap.av line 19
  5. def OAI.GeneralMahler.SCal.Mid.Cap.fl line 20
  6. def OAI.GeneralMahler.SCal.Mid.ddf line 22
  7. structure OAI.GeneralMahler.SCal.Mid.Guard line 23
  8. lemma OAI.GeneralMahler.SCal.Mid.mkGuard line 31
  9. lemma OAI.GeneralMahler.SCal.Mid.Guard.Df line 41
  10. lemma OAI.GeneralMahler.SCal.Mid.Guard.Db line 42
  11. lemma OAI.GeneralMahler.SCal.Mid.Guard.nn line 43
  12. lemma OAI.GeneralMahler.SCal.Mid.Guard.const line 46
  13. lemma OAI.GeneralMahler.SCal.Mid.Guard.absAdd line 49
  14. lemma OAI.GeneralMahler.SCal.Mid.Guard.absMul line 50
  15. lemma OAI.GeneralMahler.SCal.Mid.Guard.plus line 52
  16. lemma OAI.GeneralMahler.SCal.Mid.Guard.opp line 56
  17. lemma OAI.GeneralMahler.SCal.Mid.Guard.minus line 60
  18. lemma OAI.GeneralMahler.SCal.Mid.Guard.prod line 62
  19. lemma OAI.GeneralMahler.SCal.Mid.Guard.sq line 81