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

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Circular profile and layer bound envelopes.

  1. abbrev OAI.GeneralMahler.SCal.lc line 10
  2. abbrev OAI.GeneralMahler.SCal.ls line 11
  3. lemma OAI.GeneralMahler.SCal.lc_e line 12
  4. lemma OAI.GeneralMahler.SCal.ls_e line 13
  5. lemma OAI.GeneralMahler.SCal.lcsq line 14
  6. lemma OAI.GeneralMahler.SCal.dlc line 17
  7. lemma OAI.GeneralMahler.SCal.dls line 21
  8. def OAI.GeneralMahler.SCal.ca line 25
  9. def OAI.GeneralMahler.SCal.cb1 line 26
  10. lemma OAI.GeneralMahler.SCal.NC_c line 27
  11. lemma OAI.GeneralMahler.SCal.NC_s line 34
  12. def OAI.GeneralMahler.SCal.ro2 line 42
  13. lemma OAI.GeneralMahler.SCal.nr2 line 43
  14. def OAI.GeneralMahler.SCal.aY line 45
  15. def OAI.GeneralMahler.SCal.rPoly line 46
  16. lemma OAI.GeneralMahler.SCal.uA line 48
  17. lemma OAI.GeneralMahler.SCal.rx_eq line 55
  18. lemma OAI.GeneralMahler.SCal.ri0 line 56
  19. lemma OAI.GeneralMahler.SCal.rPolyMono line 61
  20. lemma OAI.GeneralMahler.SCal.th_m line 85
  21. lemma OAI.GeneralMahler.SCal.r_monoP line 95
  22. lemma OAI.GeneralMahler.SCal.ro2_neg line 100
  23. def OAI.GeneralMahler.SCal.omegaB line 103
  24. def OAI.GeneralMahler.SCal.rBox line 104
  25. lemma OAI.GeneralMahler.SCal.mroB line 109
  26. def OAI.GeneralMahler.SCal.rPanel line 116
  27. def OAI.GeneralMahler.SCal.testPn line 118

    Source comment

    finite arithmetic at upper cells
    def testPn (k:Nat):Bool:=
…
  28. lemma OAI.GeneralMahler.SCal.pnT line 121
  29. lemma OAI.GeneralMahler.SCal.rp_pos line 122
  30. lemma OAI.GeneralMahler.SCal.rp_val line 124