OAI/Probability/SignedSweeps/YoungLemma.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.fin_strictMono_val_le line 11
  2. lemma OAI.SignedSweeps.fin_injective_sum_lower line 24
  3. lemma OAI.SignedSweeps.fin_injective_minimal_sum line 36
  4. lemma OAI.SignedSweeps.Partition.rowOf_lt line 65
  5. lemma OAI.SignedSweeps.Partition.colOf_lt_rowLen line 69
  6. def OAI.SignedSweeps.Partition.rowEquiv line 73
  7. lemma OAI.SignedSweeps.Partition.rowOf_rowEquiv line 85
  8. lemma OAI.SignedSweeps.Partition.colOf_rowEquiv line 89
  9. lemma OAI.SignedSweeps.Partition.injective_pair line 93
  10. lemma OAI.SignedSweeps.young_column_bound line 108
  11. lemma OAI.SignedSweeps.young_factorization line 138
  12. lemma OAI.SignedSweeps.young_collision line 160