OAI/Geometry/Convex/GeneralMahler/Mills.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

§03 scalar log-Jacobian weights. Antitonicity of W via an elementary argument that integration from -∞ preserves log concavity.

  1. lemma OAI.GeneralMahler.rapid.tail_limit_bot line 11
  2. lemma OAI.GeneralMahler.Layers.pbot line 21
  3. lemma OAI.GeneralMahler.Layers.ptop line 25
  4. lemma OAI.GeneralMahler.Layers.abot line 31
  5. lemma OAI.GeneralMahler.Layers.abot' line 39
  6. def OAI.GeneralMahler.Layers.MillsC line 42
  7. def OAI.GeneralMahler.Layers.MillsJ line 43
  8. def OAI.GeneralMahler.Layers.MillsW line 44
  9. lemma OAI.GeneralMahler.Layers.mc_pos line 46
  10. lemma OAI.GeneralMahler.Layers.mj_eq line 47
  11. lemma OAI.GeneralMahler.Layers.mj_pos line 52
  12. lemma OAI.GeneralMahler.Layers.mw_pos line 53
  13. lemma OAI.GeneralMahler.Layers.d_mc line 55
  14. lemma OAI.GeneralMahler.Layers.d_mj line 58
  15. lemma OAI.GeneralMahler.Layers.d_mw line 61
  16. lemma OAI.GeneralMahler.Layers.c_mc line 65
  17. lemma OAI.GeneralMahler.Layers.c_mj line 66
  18. lemma OAI.GeneralMahler.Layers.c_mw line 67
  19. lemma OAI.GeneralMahler.Layers.mc_anti line 68
  20. lemma OAI.GeneralMahler.Layers.mw_le line 72

    Source comment

    log-concavity of p implies that of its primitive a and again of ∫a
    lemma mw_le (x:ℝ) : MillsW x ≤ 1 := by
…

    Mentions: OAI.GeneralMahler.Layers.MillsW

  21. lemma OAI.GeneralMahler.Layers.mj_mono line 93
  22. lemma OAI.GeneralMahler.Layers.mw_anti line 97
  23. lemma OAI.GeneralMahler.Layers.mc_lip line 134
  24. lemma OAI.GeneralMahler.Layers.poly_mc line 142
  25. lemma OAI.GeneralMahler.Layers.poly_mj line 143
  26. lemma OAI.GeneralMahler.Layers.poly_mw line 144
  27. lemma OAI.GeneralMahler.Layers.rapid_mcs line 146
  28. lemma OAI.GeneralMahler.Layers.rapid_mws line 158
  29. lemma OAI.GeneralMahler.Layers.limit_mc line 162
  30. lemma OAI.GeneralMahler.Layers.mw_tail line 166