OAI/Geometry/Convex/GeneralMahler/pRapid.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Scalar tail estimates near §02.

  1. lemma OAI.GeneralMahler.rapid_exp_sq line 11
  2. lemma OAI.GeneralMahler.rapid.product line 29
  3. lemma OAI.GeneralMahler.rapid.mono line 39
  4. lemma OAI.GeneralMahler.rapid.tail_limit line 43
  5. lemma OAI.GeneralMahler.rapid.integrable_real line 54
  6. lemma OAI.GeneralMahler.Layers.rapid_phi line 60
  7. lemma OAI.GeneralMahler.Layers.p_small line 66
  8. def OAI.GeneralMahler.Layers.st line 82
  9. lemma OAI.GeneralMahler.Layers.measurable_st line 83
  10. lemma OAI.GeneralMahler.Layers.rapid_p line 86
  11. lemma OAI.GeneralMahler.Layers.poly_a line 97
  12. lemma OAI.GeneralMahler.Layers.ratio_bound line 105

    Source comment

    ratio p/a used in μ tail moment proof
    lemma ratio_bound : PolyBound (fun x => p x / a x) := by
…

    Mentions: OAI.GeneralMahler.PolyBound, OAI.GeneralMahler.Layers.p, OAI.GeneralMahler.Layers.a