OAI/Combinatorics/MatchingEntropy/Optimizer.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingEntropyBounds.entropy_mix_ge line 16
  2. theorem OAI.MatchingEntropyBounds.entropy_mix_zero_bonus line 28
  3. theorem OAI.MatchingEntropyBounds.entropy_maximizer_support line 50
  4. theorem OAI.MatchingEntropyBounds.matching_optimizer_support line 74
  5. theorem OAI.MatchingEntropyBounds.negMulLog_tangent line 91
  6. theorem OAI.MatchingEntropyBounds.entropy_le_crossEntropy line 104
  7. theorem OAI.MatchingEntropyBounds.entropy_line_hasDerivAt line 119
  8. theorem OAI.MatchingEntropyBounds.matching_optimizer_log_annihilates line 142
  9. theorem OAI.MatchingEntropyBounds.exists_pos_nonneg_perturb line 173
  10. theorem OAI.MatchingEntropyBounds.matching_optimizer_face_support line 197