OAI/Geometry/PolarProducts/LogProfile.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLogProfile.cutoff line 38
2. def OAI.SmoothLogProfile.slope line 40
3. def OAI.SmoothLogProfile.profile line 42
4. theorem OAI.SmoothLogProfile.cutoff_smooth line 44
5. theorem OAI.SmoothLogProfile.slope_smooth line 47
6. theorem OAI.SmoothLogProfile.cutoff_mem line 50
7. theorem OAI.SmoothLogProfile.cutoff_zero line 53
8. theorem OAI.SmoothLogProfile.cutoff_one line 57
9. theorem OAI.SmoothLogProfile.cutoff_monotone line 61
10. theorem OAI.SmoothLogProfile.slope_left line 66
11. theorem OAI.SmoothLogProfile.slope_right line 69
12. theorem OAI.SmoothLogProfile.slope_pos line 72
13. theorem OAI.SmoothLogProfile.slope_monotone line 82
14. theorem OAI.SmoothLogProfile.hasDerivAt_profile line 98
15. theorem OAI.SmoothLogProfile.deriv_profile line 106
16. theorem OAI.SmoothLogProfile.profile_smooth line 109
17. theorem OAI.SmoothLogProfile.deriv_profile_pos line 114
18. theorem OAI.SmoothLogProfile.second_deriv_profile_nonneg line 118
19. theorem OAI.SmoothLogProfile.profile_sub line 123
20. theorem OAI.SmoothLogProfile.profile_right line 131
21. theorem OAI.SmoothLogProfile.profile_left line 142
22. theorem OAI.ComplexPotential.exists_ball_from_holomorphic_zero line 168