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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Uniform global (after 64) certificates of value and Euler derivative bounds.

  1. lemma OAI.GeneralMahler.SCal.Tail.checkKR line 9

    Source comment

    K needs individual scaled-error bounds because tends to zero
    private lemma checkKR: SubB (bKR 0) (band (-500) 500) &&
    SubB (bKR 1) (band (-5000) 5000) &&
    SubB (bKR 2) (band (-15000) 15000) := by decide +kernel
  2. lemma OAI.GeneralMahler.SCal.Tail.kTail line 13
  3. def OAI.GeneralMahler.SCal.Tail.ivb line 44

    Source comment

    profiles v' correction and v''
    def ivb:IV:= IV.span 0 ((1:IV)/IV.c 64)
  4. def OAI.GeneralMahler.SCal.Tail.mxB line 45
  5. def OAI.GeneralMahler.SCal.Tail.rvb line 46
  6. def OAI.GeneralMahler.SCal.Tail.vvb line 47
  7. lemma OAI.GeneralMahler.SCal.Tail.vTail line 48
  8. def OAI.GeneralMahler.SCal.Tail.tabT line 81
  9. lemma OAI.GeneralMahler.SCal.Tail.tag_tail line 99
  10. theorem OAI.GeneralMahler.SCal.Tail.tailCheck line 135
  11. theorem OAI.GeneralMahler.SCal.Tail.tailXCheck line 136
  12. lemma OAI.GeneralMahler.SCal.Tail.rad_tail line 139