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

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Range assertions and combined first derivative assertion for §07. Integers in tables denote exact multiples 1/10000.

  1. def OAI.GeneralMahler.SCal.Grid.bandD line 12

    Source comment

    exact scale
    def bandD : Int:=den / 10000
  2. def OAI.GeneralMahler.SCal.Grid.bd line 13
  3. def OAI.GeneralMahler.SCal.Grid.band line 14
  4. lemma OAI.GeneralMahler.SCal.Grid.w_bd line 15
  5. lemma OAI.GeneralMahler.SCal.Grid.mem_band line 16
  6. lemma OAI.GeneralMahler.SCal.Grid.mbd line 19
  7. def OAI.GeneralMahler.SCal.Grid.rng line 21
  8. def OAI.GeneralMahler.SCal.Grid.roff line 38
  9. structure OAI.GeneralMahler.SCal.Grid.Panel line 47
  10. def OAI.GeneralMahler.SCal.Grid.pan line 54
  11. def OAI.GeneralMahler.SCal.Grid.panel line 56
  12. def OAI.GeneralMahler.SCal.Grid.stage line 66
  13. def OAI.GeneralMahler.SCal.Grid.checkSR line 70
  14. def OAI.GeneralMahler.SCal.Grid.SIn line 72
  15. lemma OAI.GeneralMahler.SCal.Grid.SIn_check line 74
  16. def OAI.GeneralMahler.SCal.Grid.Ucost line 78
  17. def OAI.GeneralMahler.SCal.Grid.Ubox line 82
  18. def OAI.GeneralMahler.SCal.Grid.Ur line 85
  19. def OAI.GeneralMahler.SCal.Grid.UrB line 86
  20. def OAI.GeneralMahler.SCal.Grid.Cor line 87
  21. def OAI.GeneralMahler.SCal.Grid.Ta line 88
  22. def OAI.GeneralMahler.SCal.Grid.CorB line 89
  23. def OAI.GeneralMahler.SCal.Grid.TaB line 90
  24. lemma OAI.GeneralMahler.SCal.Grid.mUcost line 91
  25. lemma OAI.GeneralMahler.SCal.Grid.mUr line 100
  26. lemma OAI.GeneralMahler.SCal.Grid.mCor line 105
  27. lemma OAI.GeneralMahler.SCal.Grid.mTa line 110
  28. def OAI.GeneralMahler.SCal.Grid.Corr line 115
  29. def OAI.GeneralMahler.SCal.Grid.joint line 118
  30. lemma OAI.GeneralMahler.SCal.Grid.c_check line 123
  31. def OAI.GeneralMahler.SCal.Grid.allT line 131
  32. lemma OAI.GeneralMahler.SCal.Grid.allT_mem line 132
  33. def OAI.GeneralMahler.SCal.Grid.checkIn line 133
  34. lemma OAI.GeneralMahler.SCal.Grid.hasSub line 134
  35. def OAI.GeneralMahler.SCal.Grid.x5 line 137
  36. def OAI.GeneralMahler.SCal.Grid.pass0 line 138
  37. def OAI.GeneralMahler.SCal.Grid.pass line 144
  38. structure OAI.GeneralMahler.SCal.Grid.passR line 146
  39. lemma OAI.GeneralMahler.SCal.Grid.passes line 153
  40. lemma OAI.GeneralMahler.SCal.Grid.cell_R line 163
  41. lemma OAI.GeneralMahler.SCal.Grid.cell_pass line 170