OAI/Combinatorics/MatchingEntropy/Components.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.Refined.underlyingSimple line 16
  2. abbrev OAI.MatchingEntropyBounds.Refined.Component line 25
  3. instance OAI.MatchingEntropyBounds.Refined.componentFintype line 26
  4. instance OAI.MatchingEntropyBounds.Refined.componentDecidableEq line 27
  5. def OAI.MatchingEntropyBounds.Refined.componentOf line 29
  6. theorem OAI.MatchingEntropyBounds.Refined.component_edge_eq line 33
  7. def OAI.MatchingEntropyBounds.Refined.componentGraph line 37
  8. def OAI.MatchingEntropyBounds.Refined.componentMean line 43
  9. def OAI.MatchingEntropyBounds.Refined.componentOrder line 46
  10. def OAI.MatchingEntropyBounds.Refined.piLaw line 53
  11. theorem OAI.MatchingEntropyBounds.Refined.piLaw_simplex line 56
  12. theorem OAI.MatchingEntropyBounds.Refined.piLaw_expect line 65
  13. theorem OAI.MatchingEntropyBounds.Refined.piLaw_marginal line 92
  14. theorem OAI.MatchingEntropyBounds.Refined.piLaw_crossEntropy line 98
  15. theorem OAI.MatchingEntropyBounds.Refined.entropy_piLaw line 113
  16. theorem OAI.MatchingEntropyBounds.Refined.entropy_le_marginal_sum line 120
  17. theorem OAI.MatchingEntropyBounds.Refined.component_incident_iff line 136
  18. theorem OAI.MatchingEntropyBounds.Refined.component_eq_of_incident line 148
  19. def OAI.MatchingEntropyBounds.Refined.componentRestrict line 154
  20. theorem OAI.MatchingEntropyBounds.Refined.mem_componentRestrict line 166
  21. theorem OAI.MatchingEntropyBounds.Refined.componentRestrict_indicator line 172
  22. def OAI.MatchingEntropyBounds.Refined.componentGlue line 177
  23. theorem OAI.MatchingEntropyBounds.Refined.mem_componentGlue line 194
  24. def OAI.MatchingEntropyBounds.Refined.componentMatchingEquiv line 202
  25. theorem OAI.MatchingEntropyBounds.Refined.component_mean_marginal line 218
  26. theorem OAI.MatchingEntropyBounds.Refined.component_feasible line 227
  27. theorem OAI.MatchingEntropyBounds.Refined.fiberMass_comp line 235
  28. theorem OAI.MatchingEntropyBounds.Refined.component_joint_entropy_bound line 243
  29. theorem OAI.MatchingEntropyBounds.Refined.component_product_feasible line 251
  30. theorem OAI.MatchingEntropyBounds.Refined.component_maxEntropy line 270
  31. theorem OAI.MatchingEntropyBounds.Refined.component_entropy_terms line 286
  32. theorem OAI.MatchingEntropyBounds.Refined.component_additivity line 293
  33. theorem OAI.MatchingEntropyBounds.Refined.fractional_components line 311