OAI/Probability/BinarySweep/GridBounds/GridSplit.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryCoordinateSweeps.GridSplit.leftBits line 15
  2. abbrev OAI.BinaryCoordinateSweeps.GridSplit.rightBits line 16
  3. def OAI.BinaryCoordinateSweeps.GridSplit.leftSlot line 17
  4. def OAI.BinaryCoordinateSweeps.GridSplit.rightSlot line 18
  5. def OAI.BinaryCoordinateSweeps.GridSplit.joinSlot line 19
  6. def OAI.BinaryCoordinateSweeps.GridSplit.slotEquiv line 22
  7. lemma OAI.BinaryCoordinateSweeps.GridSplit.size_split line 35
  8. def OAI.BinaryCoordinateSweeps.GridSplit.leftTime line 39
  9. def OAI.BinaryCoordinateSweeps.GridSplit.rightTime line 40
  10. lemma OAI.BinaryCoordinateSweeps.GridSplit.rightSlot_leftTime line 44
  11. lemma OAI.BinaryCoordinateSweeps.GridSplit.leftSlot_rightTime line 54
  12. abbrev OAI.BinaryCoordinateSweeps.GridSplit.RowLabels line 67
  13. abbrev OAI.BinaryCoordinateSweeps.GridSplit.ColumnLabels line 69
  14. instance OAI.BinaryCoordinateSweeps.GridSplit.rowLabelsFintype line 72
  15. instance OAI.BinaryCoordinateSweeps.GridSplit.columnLabelsFintype line 74
  16. def OAI.BinaryCoordinateSweeps.GridSplit.rowFamily line 77
  17. def OAI.BinaryCoordinateSweeps.GridSplit.columnFamily line 96
  18. def OAI.BinaryCoordinateSweeps.GridSplit.fillSlot line 124
  19. lemma OAI.BinaryCoordinateSweeps.GridSplit.fillSlot_other line 127
  20. def OAI.BinaryCoordinateSweeps.GridSplit.leftOutsideEquiv line 131
  21. def OAI.BinaryCoordinateSweeps.GridSplit.rightOutsideEquiv line 153
  22. def OAI.BinaryCoordinateSweeps.GridSplit.rowChoices line 175
  23. def OAI.BinaryCoordinateSweeps.GridSplit.columnChoices line 177
  24. def OAI.BinaryCoordinateSweeps.GridSplit.joinChoices line 180
  25. def OAI.BinaryCoordinateSweeps.GridSplit.choicesEquiv line 185