OAI/Combinatorics/MatchingEntropy/SeparableVariation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

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