OAI/Combinatorics/MatchingEntropy/Pointwise.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingEntropyBounds.Refined.pointwise_entropy line 18

    Distinct definitions of this name: ComparatorChallenges/MatchingEntropyBounds.lean:73 (different declaration text). Qualify references as OAI.MatchingEntropyBounds.Refined.pointwise_entropy@path.

  2. theorem OAI.MatchingEntropyBounds.Refined.F_nonneg line 27
  3. theorem OAI.MatchingEntropyBounds.Refined.B_nonneg line 33
  4. theorem OAI.MatchingEntropyBounds.Refined.B_le_order line 40
  5. theorem OAI.MatchingEntropyBounds.Refined.entropy_defect line 48
  6. def OAI.MatchingEntropyBounds.Refined.uniformLaw line 69
  7. theorem OAI.MatchingEntropyBounds.Refined.uniformLaw_simplex line 71
  8. theorem OAI.MatchingEntropyBounds.Refined.uniformLaw_entropy line 76
  9. theorem OAI.MatchingEntropyBounds.Refined.uniformMatching_mean line 84
  10. theorem OAI.MatchingEntropyBounds.Refined.continuous_binaryEntropy line 94
  11. theorem OAI.MatchingEntropyBounds.Refined.optimized_entropy line 97
  12. def OAI.MatchingEntropyBounds.Refined.countBound line 130
  13. theorem OAI.MatchingEntropyBounds.Refined.matching_nonempty_of_mem line 138
  14. theorem OAI.MatchingEntropyBounds.Refined.entropy_uniform line 145
  15. theorem OAI.MatchingEntropyBounds.Refined.finiteCount_eq_exp line 168
  16. theorem OAI.MatchingEntropyBounds.Refined.log_uniform_loss line 180
  17. theorem OAI.MatchingEntropyBounds.Refined.refined_uniform_count line 194
  18. theorem OAI.MatchingEntropyBounds.Refined.structural_count line 229
  19. theorem OAI.MatchingEntropyBounds.Refined.regular_count line 237
  20. theorem OAI.MatchingEntropyBounds.Refined.degree_cut_count line 246
  21. theorem OAI.MatchingEntropyBounds.Refined.connected_odd_cut line 267
  22. theorem OAI.MatchingEntropyBounds.Refined.connected_regular_count line 284
  23. def OAI.MatchingEntropyBounds.Refined.weightedPartition line 291
  24. def OAI.MatchingEntropyBounds.Refined.weightedObjective line 293
  25. def OAI.MatchingEntropyBounds.Refined.gibbsLaw line 295
  26. theorem OAI.MatchingEntropyBounds.Refined.weightedPartition_pos line 299
  27. theorem OAI.MatchingEntropyBounds.Refined.gibbsLaw_pos line 305
  28. theorem OAI.MatchingEntropyBounds.Refined.gibbsLaw_simplex line 310
  29. theorem OAI.MatchingEntropyBounds.Refined.gibbs_cross_entropy line 317
  30. theorem OAI.MatchingEntropyBounds.Refined.gibbs_law_bound line 330
  31. theorem OAI.MatchingEntropyBounds.Refined.gibbs_law_equality line 343
  32. theorem OAI.MatchingEntropyBounds.Refined.gibbs_variational line 355
  33. theorem OAI.MatchingEntropyBounds.Refined.weighted_count line 374