OAI/Geometry/Convex/GeneralMahler/Intervals/Jet.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Real and interval towers of higher derivatives.

  1. abbrev OAI.GeneralMahler.Jet.J line 8
  2. def OAI.GeneralMahler.Jet.tail line 9
  3. def OAI.GeneralMahler.Jet.ray line 10
  4. def OAI.GeneralMahler.Jet.plusJ line 13
  5. def OAI.GeneralMahler.Jet.subJ line 14
  6. def OAI.GeneralMahler.Jet.negJ line 15
  7. def OAI.GeneralMahler.Jet.mulJ0 line 17
  8. def OAI.GeneralMahler.Jet.mulJ line 20
  9. def OAI.GeneralMahler.Jet.cpM line 23

    Source comment

    returns derivative of f(x)*y with f derivatives supplied by w
    def cpM {α} [Add α] [Mul α]: ℕ→J α→J α→J α→α
  | 0,w,_,y=> w 0*y 0
  | n+1,w,x,y=> cpM n (tail w) x (mulJ (tail x) y) + cpM n w x (tail y)

    Mentions: OAI.GeneralMahler.Jet.J, OAI.GeneralMahler.Jet.tail, OAI.GeneralMahler.Jet.mulJ

  10. def OAI.GeneralMahler.Jet.compJ line 26
  11. abbrev OAI.GeneralMahler.Jet.RF line 31

    Source comment

    pointwise tower of derivative functions on S
    abbrev RF:=ℝ→J ℝ

    Mentions: OAI.GeneralMahler.Jet.J

  12. def OAI.GeneralMahler.Jet.TW line 32
  13. lemma OAI.GeneralMahler.Jet.TW.mono line 36
  14. lemma OAI.GeneralMahler.Jet.TW.tail line 37
  15. lemma OAI.GeneralMahler.Jet.TW.add line 38
  16. lemma OAI.GeneralMahler.Jet.TW.sub line 40
  17. lemma OAI.GeneralMahler.Jet.TW.neg line 42
  18. lemma OAI.GeneralMahler.Jet.TW.const line 43
  19. lemma OAI.GeneralMahler.Jet.TW.mul line 47
  20. lemma OAI.GeneralMahler.Jet.TW.cp line 53
  21. lemma OAI.GeneralMahler.Jet.TW.comp line 63
  22. def OAI.GeneralMahler.Jet.dV line 69
  23. lemma OAI.GeneralMahler.Jet.V_eq line 72
  24. instance OAI.GeneralMahler.Jet.(instance at line 84) line 84
  25. def OAI.GeneralMahler.Jet.Fits line 85
  26. lemma OAI.GeneralMahler.Jet.Fits.ray line 87
  27. lemma OAI.GeneralMahler.Jet.Fits.drop line 91
  28. lemma OAI.GeneralMahler.Jet.Fits.add line 92
  29. lemma OAI.GeneralMahler.Jet.Fits.sub line 94
  30. lemma OAI.GeneralMahler.Jet.Fits.neg line 96
  31. lemma OAI.GeneralMahler.Jet.Fits.mul line 97
  32. lemma OAI.GeneralMahler.Jet.Fits.cp line 101
  33. lemma OAI.GeneralMahler.Jet.Fits.comp line 106