OAI/Combinatorics/PerfectMatching/Separable.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropy.binaryEntropy line 16
  2. def OAI.MatchingEntropy.separableLower line 18
  3. def OAI.MatchingEntropy.structuralBase line 20
  4. theorem OAI.MatchingEntropy.continuous_separableLower line 24
  5. def OAI.MatchingEntropy.separableLineD line 27
  6. theorem OAI.MatchingEntropy.separable_line_eventually_hasDerivAt line 31
  7. theorem OAI.MatchingEntropy.separableLineD_hasDerivAt line 55
  8. theorem OAI.MatchingEntropy.separable_second_variation line 67
  9. theorem OAI.MatchingEntropy.mean_score_one line 96
  10. theorem OAI.MatchingEntropy.matching_separable_second_variation line 120