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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Compact certificate for §07 and table for later quadrature.

  1. structure OAI.GeneralMahler.SCal.Grid.Line line 10
  2. def OAI.GeneralMahler.SCal.Grid.dn8 line 20
  3. def OAI.GeneralMahler.SCal.Grid.GB line 21
  4. def OAI.GeneralMahler.SCal.Grid.GP line 22
  5. def OAI.GeneralMahler.SCal.Grid.gv line 23
  6. lemma OAI.GeneralMahler.SCal.Grid.mGP line 24
  7. def OAI.GeneralMahler.SCal.Grid.inData line 29
  8. def OAI.GeneralMahler.SCal.Grid.checkL line 36
  9. structure OAI.GeneralMahler.SCal.Grid.NodeTrue line 39
  10. lemma OAI.GeneralMahler.SCal.Grid.nodeC line 46
  11. lemma OAI.GeneralMahler.SCal.Grid.line_good line 58
  12. def OAI.GeneralMahler.SCal.Grid.runB line 70

    Source comment

    The check recurses on the number of grid cells.
    def runB (p:ℕ→Bool) (n:ℕ):ℕ→Bool
  | 0=>true
  | r+1=> p (n+r)&&runB p n r
  13. def OAI.GeneralMahler.SCal.Grid.By line 73
  14. lemma OAI.GeneralMahler.SCal.Grid.byRun line 74
  15. lemma OAI.GeneralMahler.SCal.Grid.byJoin line 83