OAI/Geometry/Convex/GeneralMahler/Growth.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Elementary bounds used throughout the Gaussian and layer integrations. We keep pointwise growth and measurability hypotheses separate.

  1. def OAI.GeneralMahler.PolyBound line 14
  2. theorem OAI.GeneralMahler.PolyBound.of_bound line 19
  3. theorem OAI.GeneralMahler.PolyBound.const line 22
  4. theorem OAI.GeneralMahler.PolyBound.id line 24
  5. theorem OAI.GeneralMahler.PolyBound.clm line 27
  6. theorem OAI.GeneralMahler.PolyBound.mono line 33
  7. lemma OAI.GeneralMahler.PolyBound.raise_le line 38
  8. lemma OAI.GeneralMahler.PolyBound.common line 40
  9. theorem OAI.GeneralMahler.PolyBound.add line 49
  10. theorem OAI.GeneralMahler.PolyBound.neg line 53
  11. theorem OAI.GeneralMahler.PolyBound.sub line 54
  12. theorem OAI.GeneralMahler.PolyBound.norm line 56
  13. lemma OAI.GeneralMahler.PolyBound.of_prod_le line 58
  14. theorem OAI.GeneralMahler.PolyBound.smul line 67
  15. theorem OAI.GeneralMahler.PolyBound.mul line 70
  16. theorem OAI.GeneralMahler.PolyBound.pow line 73
  17. theorem OAI.GeneralMahler.PolyBound.prodMk line 78
  18. theorem OAI.GeneralMahler.PolyBound.fst line 82
  19. theorem OAI.GeneralMahler.PolyBound.snd line 83
  20. theorem OAI.GeneralMahler.PolyBound.comp line 84
  21. theorem OAI.GeneralMahler.PolyBound.linear_growth line 95
  22. theorem OAI.GeneralMahler.PolyBound.lipschitz line 103
  23. theorem OAI.GeneralMahler.PolyBound.indicator line 107
  24. lemma OAI.GeneralMahler.integrable_envelope line 121
  25. theorem OAI.GeneralMahler.PolyBound.gaussian_integrable line 134