OAI/Combinatorics/MatchingEntropy/EntropyUpper.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingEntropyBounds.entropy_le_subprob_crossEntropy line 14
  2. def OAI.MatchingEntropyBounds.LooplessGraph.matchingBits line 33
  3. theorem OAI.MatchingEntropyBounds.LooplessGraph.matchingBits_injective line 37
  4. def OAI.MatchingEntropyBounds.productBoolean line 46
  5. theorem OAI.MatchingEntropyBounds.productBoolean_nonneg line 50
  6. theorem OAI.MatchingEntropyBounds.productBoolean_sum line 59
  7. theorem OAI.MatchingEntropyBounds.matchingBoolean_sum_le line 65
  8. theorem OAI.MatchingEntropyBounds.matching_boolean_factor_pos line 79
  9. theorem OAI.MatchingEntropyBounds.matching_entropy_le_binary line 105
  10. theorem OAI.MatchingEntropyBounds.maxMatchingEntropy_le_binary line 143