OAI/Geometry/Convex/GeneralMahler/Scalar/Moments.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

§07 stable Laplace moments. Define using the translated Gaussian variable on (x,∞).

  1. def OAI.GeneralMahler.SCal.Lpn line 11
  2. def OAI.GeneralMahler.SCal.Ymk line 12
  3. lemma OAI.GeneralMahler.SCal.lp_r line 13
  4. lemma OAI.GeneralMahler.SCal.lp_i line 17
  5. lemma OAI.GeneralMahler.SCal.Ymp line 21
  6. lemma OAI.GeneralMahler.SCal.Ym0 line 29
  7. lemma OAI.GeneralMahler.SCal.Hd0 line 32
  8. lemma OAI.GeneralMahler.SCal.Hdn line 37
  9. lemma OAI.GeneralMahler.SCal.R0 line 44
  10. lemma OAI.GeneralMahler.SCal.Rn line 54
  11. lemma OAI.GeneralMahler.SCal.DYmk0 line 63
  12. lemma OAI.GeneralMahler.SCal.DYmk line 67
  13. lemma OAI.GeneralMahler.SCal.Yanti line 88
  14. def OAI.GeneralMahler.SCal.cRat line 92

    Source comment

    continued fraction
    def cRat (n:Nat) (x:ℝ):= Ymk (n+1) x/Ymk n x

    Mentions: OAI.GeneralMahler.SCal.Ymk

  15. lemma OAI.GeneralMahler.SCal.cRp line 93
  16. lemma OAI.GeneralMahler.SCal.cfBase line 94
  17. lemma OAI.GeneralMahler.SCal.cfIter line 96