OAI/Combinatorics/MatchingEntropy/Coupling.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.fiberMass line 16
  2. theorem OAI.MatchingEntropyBounds.fiberMass_nonneg line 19
  3. theorem OAI.MatchingEntropyBounds.le_fiberMass_self line 26
  4. def OAI.MatchingEntropyBounds.jointLaw line 34
  5. theorem OAI.MatchingEntropyBounds.jointLaw_nonneg line 38
  6. theorem OAI.MatchingEntropyBounds.jointLaw_first line 46
  7. theorem OAI.MatchingEntropyBounds.jointLaw_second line 66
  8. theorem OAI.MatchingEntropyBounds.jointLaw_mem_simplex line 86
  9. theorem OAI.MatchingEntropyBounds.sum_subtype_supported line 95
  10. theorem OAI.MatchingEntropyBounds.compatible_jointLaw_mem_simplex line 104
  11. theorem OAI.MatchingEntropyBounds.fiberMass_sum line 114
  12. theorem OAI.MatchingEntropyBounds.fiberMass_expect line 120
  13. theorem OAI.MatchingEntropyBounds.fiberMass_mem_simplex line 131
  14. theorem OAI.MatchingEntropyBounds.jointLaw_expect_first line 136
  15. theorem OAI.MatchingEntropyBounds.jointLaw_expect_second line 143
  16. theorem OAI.MatchingEntropyBounds.compatible_jointLaw_expect_first line 150
  17. theorem OAI.MatchingEntropyBounds.compatible_jointLaw_expect_second line 160