OAI/Probability/SignedSweeps/RowSymmetry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.diagram_rowLens_sum line 11
  2. lemma OAI.SignedSweeps.partition_rowLens_sum line 22
  3. lemma OAI.SignedSweeps.sorted_drop_term_bound line 25
  4. def OAI.SignedSweeps.truncatePartition line 40
  5. lemma OAI.SignedSweeps.truncatePartition_rowLens line 50
  6. def OAI.SignedSweeps.partsEntropy line 57
  7. lemma OAI.SignedSweeps.partsEntropy_mono line 60
  8. lemma OAI.SignedSweeps.partsEntropy_mono_of_total line 69
  9. lemma OAI.SignedSweeps.partsEntropy_drop_bound line 80
  10. lemma OAI.SignedSweeps.signedEntropy_truncate line 98
  11. lemma OAI.SignedSweeps.remainderBudget_growth line 145
  12. lemma OAI.SignedSweeps.truncated_budget_le line 152
  13. lemma OAI.SignedSweeps.truncation_coefficient_eventually line 179