OAI/Probability/BinarySweep/Mixing/LongRowDimension.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Young.longRowCells line 15
  2. lemma OAI.BinaryCoordinateSweeps.Young.longRowCells_fixed line 27
  3. theorem OAI.BinaryCoordinateSweeps.Young.long_row_dimension line 40
  4. def OAI.BinaryCoordinateSweeps.Young.flatTail line 55
  5. def OAI.BinaryCoordinateSweeps.Young.longOriented line 56
  6. lemma OAI.BinaryCoordinateSweeps.Young.transpose_card line 59
  7. lemma OAI.BinaryCoordinateSweeps.Young.rowLens_sum line 62
  8. lemma OAI.BinaryCoordinateSweeps.Young.rowLens_head line 68
  9. lemma OAI.BinaryCoordinateSweeps.Young.rowLens_tail_sum line 79
  10. lemma OAI.BinaryCoordinateSweeps.Young.longOriented_card line 85
  11. lemma OAI.BinaryCoordinateSweeps.Young.longOriented_row line 89
  12. lemma OAI.BinaryCoordinateSweeps.Young.positive_list_tail_injective line 94
  13. def OAI.BinaryCoordinateSweeps.Young.tailCode line 119
  14. lemma OAI.BinaryCoordinateSweeps.Young.tailCode_injective line 127
  15. theorem OAI.BinaryCoordinateSweeps.Young.flatTail_card line 149