OAI/Combinatorics/MatchingEntropy/RefinedVariation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatchingEntropyBounds.Refined.continuous_lowerObjective line 19
2. def OAI.MatchingEntropyBounds.Refined.objectiveLineD line 22
3. theorem OAI.MatchingEntropyBounds.Refined.objective_line_eventually_hasDerivAt line 26
4. theorem OAI.MatchingEntropyBounds.Refined.objectiveLineD_hasDerivAt line 50
5. theorem OAI.MatchingEntropyBounds.Refined.objective_second_variation line 62
6. theorem OAI.MatchingEntropyBounds.Refined.matching_objective_second_variation line 92
7. theorem OAI.MatchingEntropyBounds.Refined.objectiveDefect_attains_max line 146
8. theorem OAI.MatchingEntropyBounds.Refined.matching_objective_covariance line 163
9. theorem OAI.MatchingEntropyBounds.Refined.lowerObjective_forced line 218
10. theorem OAI.MatchingEntropyBounds.Refined.objective_max_has_forced line 231
11. theorem OAI.MatchingEntropyBounds.Refined.coefficient_down line 271
12. theorem OAI.MatchingEntropyBounds.Refined.strict_lower_aux line 278
13. theorem OAI.MatchingEntropyBounds.Refined.refined_lower line 313
14. def OAI.MatchingEntropyBounds.Refined.matchingProduct line 334
15. theorem OAI.MatchingEntropyBounds.Refined.matchingProduct_nonneg line 338
16. theorem OAI.MatchingEntropyBounds.Refined.matchingProduct_addForced line 343
17. theorem OAI.MatchingEntropyBounds.Refined.sum_matching_incident line 356
18. theorem OAI.MatchingEntropyBounds.Refined.matchingProduct_recursion line 385
19. theorem OAI.MatchingEntropyBounds.Refined.degree_deleteEndpoints_le line 401
20. theorem OAI.MatchingEntropyBounds.Refined.matchingProduct_sum_le_aux line 413
21. theorem OAI.MatchingEntropyBounds.Refined.matchingProduct_sum_le line 445
22. theorem OAI.MatchingEntropyBounds.Refined.matching_entropy_le_F line 450
23. theorem OAI.MatchingEntropyBounds.Refined.refined_upper line 481