OAI/Combinatorics/PerfectMatching/EntropyUpper.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingEntropy.entropy_le_subprob_crossEntropy line 13
  2. def OAI.MatchingEntropy.LooplessGraph.matchingBits line 32
  3. theorem OAI.MatchingEntropy.LooplessGraph.matchingBits_injective line 36
  4. def OAI.MatchingEntropy.productBoolean line 45
  5. theorem OAI.MatchingEntropy.productBoolean_nonneg line 49
  6. theorem OAI.MatchingEntropy.productBoolean_sum line 58
  7. theorem OAI.MatchingEntropy.matchingBoolean_sum_le line 64
  8. theorem OAI.MatchingEntropy.matching_boolean_factor_pos line 78
  9. theorem OAI.MatchingEntropy.matching_entropy_le_binary line 104
  10. theorem OAI.MatchingEntropy.maxMatchingEntropy_le_binary line 142