OAI/Combinatorics/MatchingEntropy/Calculus.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.entropyLineD line 16
  2. theorem OAI.MatchingEntropyBounds.entropy_line_hasDerivAt_at line 19
  3. theorem OAI.MatchingEntropyBounds.entropy_line_deriv_eventually line 38
  4. theorem OAI.MatchingEntropyBounds.entropyLineD_hasDerivAt line 52
  5. theorem OAI.MatchingEntropyBounds.entropy_line_second line 68
  6. theorem OAI.MatchingEntropyBounds.second_deriv_quadratic_adjustment line 75
  7. theorem OAI.MatchingEntropyBounds.second_deriv_nonpos_of_local_max line 94
  8. theorem OAI.MatchingEntropyBounds.entropy_line_eventually_hasDerivAt line 106
  9. theorem OAI.MatchingEntropyBounds.score_law_eventually_simplex line 120
  10. theorem OAI.MatchingEntropyBounds.mean_score_support line 137