OAI/Probability/BinarySweep/GridBounds/GridSplitFree.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.GridSplit.left_join line 17
  2. lemma OAI.BinaryCoordinateSweeps.GridSplit.right_join line 19
  3. lemma OAI.BinaryCoordinateSweeps.GridSplit.join_left_right line 21
  4. def OAI.BinaryCoordinateSweeps.GridSplit.rowFreeEquiv line 24
  5. def OAI.BinaryCoordinateSweeps.GridSplit.columnFreeEquiv line 59
  6. abbrev OAI.BinaryCoordinateSweeps.GridSplit.RowSamples line 94
  7. abbrev OAI.BinaryCoordinateSweeps.GridSplit.ColumnSamples line 95
  8. def OAI.BinaryCoordinateSweeps.GridSplit.rowRemaining line 97
  9. def OAI.BinaryCoordinateSweeps.GridSplit.columnRemaining line 102
  10. lemma OAI.BinaryCoordinateSweeps.GridSplit.rowRemaining_val line 108
  11. lemma OAI.BinaryCoordinateSweeps.GridSplit.columnRemaining_val line 113
  12. lemma OAI.BinaryCoordinateSweeps.GridSplit.remainingBijection_split line 118
  13. def OAI.BinaryCoordinateSweeps.GridSplit.rowReference line 145
  14. def OAI.BinaryCoordinateSweeps.GridSplit.columnReference line 150
  15. def OAI.BinaryCoordinateSweeps.GridSplit.rowRelative line 155
  16. def OAI.BinaryCoordinateSweeps.GridSplit.columnRelative line 158
  17. def OAI.BinaryCoordinateSweeps.GridSplit.framePermutation line 161
  18. theorem OAI.BinaryCoordinateSweeps.GridSplit.remainingPerm_factor line 164
  19. def OAI.BinaryCoordinateSweeps.GridSplit.rowAverage line 178
  20. def OAI.BinaryCoordinateSweeps.GridSplit.columnAverage line 182
  21. theorem OAI.BinaryCoordinateSweeps.GridSplit.groupAverage_split line 188
  22. theorem OAI.BinaryCoordinateSweeps.GridSplit.conditional_evenMoment_split line 199