OAI/Probability/SignedSweeps/OccurrenceDimension.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.Partition.rowOf_lt_colLen line 11
  2. def OAI.SignedSweeps.Partition.colEquiv line 15
  3. lemma OAI.SignedSweeps.Partition.colOf_colEquiv line 27
  4. lemma OAI.SignedSweeps.Partition.sum_rowLen line 31
  5. lemma OAI.SignedSweeps.Partition.sum_colLen line 35
  6. lemma OAI.SignedSweeps.Partition.rowLen_pos line 39
  7. lemma OAI.SignedSweeps.Partition.colLen_pos line 43
  8. lemma OAI.SignedSweeps.Partition.sum_rowOf line 47
  9. lemma OAI.SignedSweeps.Partition.sum_colOf line 52
  10. lemma OAI.SignedSweeps.partsEntropy_rowLen line 65
  11. def OAI.SignedSweeps.signedColorProbability line 72
  12. lemma OAI.SignedSweeps.signedColorProbability_nonneg line 77
  13. lemma OAI.SignedSweeps.signedColorProbability_sum line 81
  14. lemma OAI.SignedSweeps.signedColorProbability_used_pos line 89
  15. lemma OAI.SignedSweeps.signedColorProbability_entropy line 104
  16. lemma OAI.SignedSweeps.partsEntropy_change_total line 127
  17. lemma OAI.SignedSweeps.partsEntropy_partition_empty line 143
  18. lemma OAI.SignedSweeps.signedEntropy_change_total line 150
  19. lemma OAI.SignedSweeps.split_entropy_le_remainder line 170
  20. lemma OAI.SignedSweeps.signedOccurrence_dimension line 179
  21. lemma OAI.SignedSweeps.spechtDimension_le_factorial line 201
  22. lemma OAI.SignedSweeps.spechtDimension_le_exp_size_log_size line 208
  23. lemma OAI.SignedSweeps.signedOccurrence_log_dimension line 216