OAI/Probability/BinarySweep/YoungTheory/YoungDominance.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Young.rowPrefix line 14
  2. def OAI.BinaryCoordinateSweeps.Young.Dominates line 17
  3. lemma OAI.BinaryCoordinateSweeps.Young.filter_column_card line 19
  4. lemma OAI.BinaryCoordinateSweeps.Young.filter_injective_column_le line 37
  5. lemma OAI.BinaryCoordinateSweeps.Young.card_filter_eq_sum_columns line 51
  6. theorem OAI.BinaryCoordinateSweeps.Young.dominates_of_column_injective line 59
  7. lemma OAI.BinaryCoordinateSweeps.Young.rowPrefix_succ line 71
  8. lemma OAI.BinaryCoordinateSweeps.Young.dominates_antisymm line 98
  9. def OAI.BinaryCoordinateSweeps.Young.crossAnti line 118
  10. lemma OAI.BinaryCoordinateSweeps.Young.crossAnti_apply line 121
  11. lemma OAI.BinaryCoordinateSweeps.Young.crossAnti_rep line 126
  12. lemma OAI.BinaryCoordinateSweeps.Young.crossAnti_basis_collision line 146
  13. theorem OAI.BinaryCoordinateSweeps.Young.crossAnti_eq_zero_of_not_dominates line 166
  14. lemma OAI.BinaryCoordinateSweeps.Young.spechtInclude_column_sum line 185
  15. theorem OAI.BinaryCoordinateSweeps.Young.intertwiner_dominance line 192
  16. theorem OAI.BinaryCoordinateSweeps.Young.equivalence_implies_diagram_eq line 206