OAI/Combinatorics/PerfectMatching/Partition.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropy.expSum line 16
  2. def OAI.MatchingEntropy.expLaw line 17
  3. lemma OAI.MatchingEntropy.expSum_pos line 19
  4. lemma OAI.MatchingEntropy.expLaw_simplex line 22
  5. lemma OAI.MatchingEntropy.log_expLaw line 27
  6. lemma OAI.MatchingEntropy.expLaw_cross line 31
  7. lemma OAI.MatchingEntropy.expSum_variational_le line 37
  8. lemma OAI.MatchingEntropy.expSum_variational_eq line 44
  9. def OAI.MatchingEntropy.LooplessGraph.score line 52
  10. def OAI.MatchingEntropy.LooplessGraph.weightedZ line 55
  11. lemma OAI.MatchingEntropy.LooplessGraph.score_indicator line 59
  12. lemma OAI.MatchingEntropy.LooplessGraph.mean_score line 64
  13. lemma OAI.MatchingEntropy.LooplessGraph.complement_entropy_le_mass line 73
  14. lemma OAI.MatchingEntropy.LooplessGraph.entropy_binary_scale line 79
  15. lemma OAI.MatchingEntropy.LooplessGraph.weighted_variational_le line 101
  16. lemma OAI.MatchingEntropy.LooplessGraph.weighted_variational_attained line 118