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

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Uniform second derivative bound of endpoint spectral averages for smooth profiles.

  1. def OAI.GeneralMahler.SCal.Mid.ment line 12
  2. def OAI.GeneralMahler.SCal.Mid.contB line 13
  3. lemma OAI.GeneralMahler.SCal.Mid.cmCont line 15
  4. lemma OAI.GeneralMahler.SCal.Mid.curC line 20
  5. lemma OAI.GeneralMahler.SCal.Mid.fmd line 25
  6. def OAI.GeneralMahler.SCal.Mid.s line 44
  7. def OAI.GeneralMahler.SCal.Mid.T0 line 45
  8. def OAI.GeneralMahler.SCal.Mid.W0 line 46
  9. def OAI.GeneralMahler.SCal.Mid.Wd line 47
  10. def OAI.GeneralMahler.SCal.Mid.denom line 48
  11. def OAI.GeneralMahler.SCal.Mid.Rg line 50
  12. def OAI.GeneralMahler.SCal.Mid.trav line 51
  13. lemma OAI.GeneralMahler.SCal.Mid.trav_eq line 52
  14. lemma OAI.GeneralMahler.SCal.Mid.dp line 57
  15. def OAI.GeneralMahler.SCal.Mid.G1 line 62
  16. def OAI.GeneralMahler.SCal.Mid.G2 line 64
  17. lemma OAI.GeneralMahler.SCal.Mid.grTrav line 69