OAI/Geometry/Convex/GeneralMahler/Middle/Tiles.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic verification of compact region.

  1. def OAI.GeneralMahler.SCal.Mid.everyF line 8
  2. lemma OAI.GeneralMahler.SCal.Mid.chk_every line 9
  3. def OAI.GeneralMahler.SCal.Mid.initC line 12
  4. def OAI.GeneralMahler.SCal.Mid.ctStep line 13
  5. lemma OAI.GeneralMahler.SCal.Mid.cWorks line 14
  6. def OAI.GeneralMahler.SCal.Mid.tile line 18

    Source comment

    Blocks left i≤280 step8, right j≤720 step8
    def tile (b:Bool)(i j:Nat):Bool:=quadRun B b 3 (8*i) (8*j)

    Mentions: OAI.GeneralMahler.SCal.Mid.quadRun

  7. def OAI.GeneralMahler.SCal.Mid.GoodS line 19
  8. def OAI.GeneralMahler.SCal.Mid.Good line 20
  9. lemma OAI.GeneralMahler.SCal.Mid.colG line 22
  10. lemma OAI.GeneralMahler.SCal.Mid.has_middle line 42