OAI/Analysis/IntegralMeans/Turning.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Brennan.secantTriangle line 21
2. lemma OAI.Brennan.convex_secantTriangle line 23
3. lemma OAI.Brennan.nonempty_secantTriangle line 36
4. def OAI.Brennan.averagedDerivative line 38
5. lemma OAI.Brennan.continuous_averagedDerivative line 41
6. lemma OAI.Brennan.sub_smul_averagedDerivative line 49
7. lemma OAI.Brennan.averagedDerivative_diag line 60
8. def OAI.Brennan.extendedSecant line 63
9. lemma OAI.Brennan.continuous_extendedSecant line 67
10. lemma OAI.Brennan.extendedSecant_diag line 73
11. lemma OAI.Brennan.extendedSecant_corner line 76
12. lemma OAI.Brennan.extendedSecant_scale line 79
13. lemma OAI.Brennan.extendedSecant_ne_zero line 95
14. lemma OAI.Brennan.periodic_deriv line 122
15. lemma OAI.Brennan.extendedSecant_edges line 129
16. lemma OAI.Brennan.extendedSecant_left_re_nonneg line 152
17. def OAI.Brennan.triangleOrigin line 171
18. def OAI.Brennan.triangleCorner line 173
19. def OAI.Brennan.triangleEnd line 175
20. lemma OAI.Brennan.exists_secant_log line 177
21. lemma OAI.Brennan.continuous_log_unique line 192
22. def OAI.Brennan.triangleLeft line 198
23. def OAI.Brennan.triangleTop line 201
24. def OAI.Brennan.triangleDiag line 204
25. lemma OAI.Brennan.continuous_triangleLeft line 207
26. lemma OAI.Brennan.continuous_triangleTop line 211
27. lemma OAI.Brennan.continuous_triangleDiag line 215
28. lemma OAI.Brennan.mem_slitPlane_of_re_nonneg line 219
29. lemma OAI.Brennan.log_neg_of_downward line 226
30. lemma OAI.Brennan.tangent_turning_log line 237
31. lemma OAI.Brennan.regular_level_sublevel_nhds line 286
32. lemma OAI.Brennan.regular_level_frequently_below line 343
33. lemma OAI.Brennan.regular_level_local_integer line 351
34. lemma OAI.Brennan.regular_level_local_integer_unique line 369
35. lemma OAI.Brennan.regular_level_integer_constant_along line 381
36. lemma OAI.Brennan.regular_level_loop_local_index line 400