OAI/Probability/BinarySweep/YoungTheory/YoungFactor.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryCoordinateSweeps.Young.Cell line 10
  2. def OAI.BinaryCoordinateSweeps.Young.row line 11
  3. def OAI.BinaryCoordinateSweeps.Young.col line 12
  4. lemma OAI.BinaryCoordinateSweeps.Young.nat_le_strictMono line 14
  5. lemma OAI.BinaryCoordinateSweeps.Young.sum_orderEmb line 27
  6. lemma OAI.BinaryCoordinateSweeps.Young.range_sum_le line 34
  7. lemma OAI.BinaryCoordinateSweeps.Young.eq_range_of_sum_eq line 41
  8. def OAI.BinaryCoordinateSweeps.Young.columnCells line 63
  9. lemma OAI.BinaryCoordinateSweeps.Young.mem_columnCells line 66
  10. lemma OAI.BinaryCoordinateSweeps.Young.row_injectiveOn_column line 69
  11. lemma OAI.BinaryCoordinateSweeps.Young.image_row_columnCells line 76
  12. lemma OAI.BinaryCoordinateSweeps.Young.card_columnCells line 91
  13. lemma OAI.BinaryCoordinateSweeps.Young.sum_row_columnCells line 96
  14. lemma OAI.BinaryCoordinateSweeps.Young.sum_columnCells_le line 101
  15. lemma OAI.BinaryCoordinateSweeps.Young.column_image_of_total_sum line 108
  16. lemma OAI.BinaryCoordinateSweeps.Young.rearranged_row_mem line 140
  17. def OAI.BinaryCoordinateSweeps.Young.fiberStabilizer line 150
  18. abbrev OAI.BinaryCoordinateSweeps.Young.rowStabilizer line 159
  19. abbrev OAI.BinaryCoordinateSweeps.Young.colStabilizer line 160
  20. lemma OAI.BinaryCoordinateSweeps.Young.row_col_intersection line 162
  21. theorem OAI.BinaryCoordinateSweeps.Young.row_col_factorization line 173
  22. theorem OAI.BinaryCoordinateSweeps.Young.row_col_alternative line 196