OAI/Geometry/Convex/GeneralMahler/EdgeBand.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Lower bound for beta on the band l∈[-z,z] for z≥0, using integration by parts against 1/W; equivalent to the subprobability argument in the paper.

  1. def OAI.GeneralMahler.Edge.BH line 16
  2. lemma OAI.GeneralMahler.Edge.BH_both line 17
  3. lemma OAI.GeneralMahler.Edge.BH_beta line 37
  4. def OAI.GeneralMahler.Edge.FF line 59
  5. def OAI.GeneralMahler.Edge.ntb line 60
  6. lemma OAI.GeneralMahler.Edge.ntb_both line 61
  7. lemma OAI.GeneralMahler.Edge.FF_upper line 64
  8. def OAI.GeneralMahler.Edge.trC line 73
  9. lemma OAI.GeneralMahler.Edge.trC_eq line 76
  10. lemma OAI.GeneralMahler.Edge.FF_lip line 78
  11. lemma OAI.GeneralMahler.Edge.FF_deriv line 82
  12. def OAI.GeneralMahler.Edge.Wi line 94
  13. lemma OAI.GeneralMahler.Edge.d_wi₀ line 95
  14. lemma OAI.GeneralMahler.Edge.d_wi line 97
  15. lemma OAI.GeneralMahler.Edge.dw_cont line 98
  16. lemma OAI.GeneralMahler.Edge.wi_cd line 102
  17. lemma OAI.GeneralMahler.Edge.dwi_nonneg line 104
  18. lemma OAI.GeneralMahler.Edge.ntb_int line 107
  19. lemma OAI.GeneralMahler.Edge.band line 118