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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

§07 log-series h in stable formulas. Remainders and smooth positive coefficients.

  1. def OAI.GeneralMahler.SCal.hden line 10

    Source comment

    scaled derivatives
    def hden (u v:ℝ):= 1-u*v
  2. def OAI.GeneralMahler.SCal.Qhv line 11
  3. def OAI.GeneralMahler.SCal.Qh line 12
  4. lemma OAI.GeneralMahler.SCal.hpden line 14
  5. lemma OAI.GeneralMahler.SCal.intH line 19
  6. lemma OAI.GeneralMahler.SCal.hdv line 25
  7. lemma OAI.GeneralMahler.SCal.hdQ line 35
  8. lemma OAI.GeneralMahler.SCal.hlog line 68
  9. def OAI.GeneralMahler.SCal.hCoef line 87

    Source comment

    rational/geometric remainder
    def hCoef (i n:Nat) : ℝ := Nat.choose (i+n) n
  10. def OAI.GeneralMahler.SCal.Rpow line 88
  11. def OAI.GeneralMahler.SCal.Rpoly line 89
  12. lemma OAI.GeneralMahler.SCal.comb line 91
  13. lemma OAI.GeneralMahler.SCal.RecPoly line 98
  14. lemma OAI.GeneralMahler.SCal.PowRec line 108
  15. lemma OAI.GeneralMahler.SCal.r_est line 115