OAI/Combinatorics/MatchingEntropy/Duality.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.partition line 16
  2. def OAI.MatchingEntropyBounds.tiltedLaw line 19
  3. theorem OAI.MatchingEntropyBounds.partition_pos line 22
  4. theorem OAI.MatchingEntropyBounds.partition_zero line 29
  5. theorem OAI.MatchingEntropyBounds.tiltedLaw_mem_simplex line 33
  6. theorem OAI.MatchingEntropyBounds.entropy_partition_bound line 41
  7. def OAI.MatchingEntropyBounds.linearScore line 70
  8. theorem OAI.MatchingEntropyBounds.sum_mean_assoc line 74
  9. theorem OAI.MatchingEntropyBounds.linearScore_expectation line 85
  10. theorem OAI.MatchingEntropyBounds.matching_entropy_dual_bound line 95
  11. theorem OAI.MatchingEntropyBounds.partition_hasDerivAt line 122
  12. theorem OAI.MatchingEntropyBounds.logPartition_hasDerivAt line 129
  13. theorem OAI.MatchingEntropyBounds.logPartition_second line 135