OAI/Combinatorics/MatchingEntropy/Entropy.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.marginalEntropy line 16
  2. theorem OAI.MatchingEntropyBounds.entropy_eq line 18
  3. theorem OAI.MatchingEntropyBounds.continuous_entropy line 22
  4. theorem OAI.MatchingEntropyBounds.entropy_nonneg line 27
  5. theorem OAI.MatchingEntropyBounds.entropy_le_log_card line 34
  6. theorem OAI.MatchingEntropyBounds.LooplessGraph.coordinate_mem_Icc line 55
  7. theorem OAI.MatchingEntropyBounds.LooplessGraph.incident_vertex_sum line 67
  8. theorem OAI.MatchingEntropyBounds.LooplessGraph.matching_incident_sum line 81
  9. theorem OAI.MatchingEntropyBounds.LooplessGraph.matching_card_twice line 93
  10. theorem OAI.MatchingEntropyBounds.LooplessGraph.matching_card line 106
  11. theorem OAI.MatchingEntropyBounds.LooplessGraph.indicator_sum line 111
  12. theorem OAI.MatchingEntropyBounds.LooplessGraph.marginal_sum line 116
  13. theorem OAI.MatchingEntropyBounds.maxMatchingEntropy_attained line 129
  14. theorem OAI.MatchingEntropyBounds.maxMatchingEntropy_nonneg line 138
  15. theorem OAI.MatchingEntropyBounds.maxMatchingEntropy_le_log_card line 145
  16. theorem OAI.MatchingEntropyBounds.entropy_le_maxMatchingEntropy line 153