OAI/Geometry/Convex/GeneralMahler/Scalar/Tail/Base.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Tail jets use log coordinate t, denoted y here. This implements D=x∂_x.

  1. def OAI.GeneralMahler.SCal.Tail.XX line 9
  2. def OAI.GeneralMahler.SCal.Tail.iv line 10
  3. def OAI.GeneralMahler.SCal.Tail.ev line 11
  4. def OAI.GeneralMahler.SCal.Tail.Mk line 12
  5. def OAI.GeneralMahler.SCal.Tail.Qp line 13
  6. def OAI.GeneralMahler.SCal.Tail.Z0 line 14
  7. def OAI.GeneralMahler.SCal.Tail.Lv line 15
  8. def OAI.GeneralMahler.SCal.Tail.Wv line 16
  9. lemma OAI.GeneralMahler.SCal.Tail.xP line 17
  10. lemma OAI.GeneralMahler.SCal.Tail.vP line 18
  11. lemma OAI.GeneralMahler.SCal.Tail.iP line 19
  12. lemma OAI.GeneralMahler.SCal.Tail.Xd0 line 20
  13. lemma OAI.GeneralMahler.SCal.Tail.vd0 line 21
  14. lemma OAI.GeneralMahler.SCal.Tail.id0 line 25
  15. lemma OAI.GeneralMahler.SCal.Tail.MkP line 28
  16. lemma OAI.GeneralMahler.SCal.Tail.M0e line 29
  17. lemma OAI.GeneralMahler.SCal.Tail.Mke line 34
  18. lemma OAI.GeneralMahler.SCal.Tail.Mk_hi line 43
  19. lemma OAI.GeneralMahler.SCal.Tail.Dmk line 54
  20. lemma OAI.GeneralMahler.SCal.Tail.Dqp line 65
  21. lemma OAI.GeneralMahler.SCal.Tail.Wd0 line 71
  22. def OAI.GeneralMahler.SCal.Tail.JT.IJ line 76
  23. def OAI.GeneralMahler.SCal.Tail.JT.Wrec line 77
  24. def OAI.GeneralMahler.SCal.Tail.JT.WW line 80
  25. def OAI.GeneralMahler.SCal.Tail.JT.Prec line 81
  26. def OAI.GeneralMahler.SCal.Tail.JT.TP line 84
  27. def OAI.GeneralMahler.SCal.Tail.JT.Mrec line 86

    Source comment

    Z=ξ^i Mk
    def Mrec:ℕ→ℕ→ℕ→ℝ→ℝ
  | 0,m,i,y=>(ev y)^i*Mk m y
  | n+1,m,i,y=> -2*i*Mrec n m i y + Mrec n (m+2) (i+1) y

    Mentions: OAI.GeneralMahler.SCal.Tail.ev, OAI.GeneralMahler.SCal.Tail.Mk

  28. def OAI.GeneralMahler.SCal.Tail.JT.TM line 89
  29. lemma OAI.GeneralMahler.SCal.Tail.JT.Ti line 91
  30. lemma OAI.GeneralMahler.SCal.Tail.JT.IJ0 line 95
  31. lemma OAI.GeneralMahler.SCal.Tail.JT.Tw line 96
  32. lemma OAI.GeneralMahler.SCal.Tail.JT.Tp line 104
  33. lemma OAI.GeneralMahler.SCal.Tail.JT.TM0 line 109
  34. lemma OAI.GeneralMahler.SCal.Tail.JT.Tm line 110