OAI/Geometry/PolarProducts/LensEstimates.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarLens.arctan_le_self line 37
2. theorem OAI.PlanarLens.half_le_arctan line 47
3. theorem OAI.PlanarLens.reciprocal_arctan line 59
4. def OAI.PlanarLens.circleTop line 94
5. theorem OAI.PlanarLens.circleTop_re line 96
6. theorem OAI.PlanarLens.circleTop_im line 100
7. theorem OAI.PlanarLens.norm_circleTop line 104
8. theorem OAI.PlanarLens.circleTop_zero line 110
9. theorem OAI.PlanarLens.circleTop_pi_half line 113
10. theorem OAI.PlanarLens.continuous_circleTop line 116
11. theorem OAI.PlanarLens.hasDerivAt_F_im_circleTop line 119
12. theorem OAI.PlanarLens.continuous_A_circleTop line 140
13. theorem OAI.PlanarLens.gap_integral line 150
14. theorem OAI.PlanarLens.A_circleTop_le line 158
15. theorem OAI.PlanarLens.gap_le_square line 175
16. theorem OAI.PlanarLens.reciprocal_A_circleTop line 202
17. theorem OAI.PlanarLens.circleTop_arg line 250
18. lemma OAI.PlanarLens.div_le_sqrt_of_gap line 264
19. theorem OAI.PlanarLens.reciprocal_A_slice line 273
20. theorem OAI.PlanarLens.deriv_T_eq line 316
21. theorem OAI.PlanarLens.deriv_T_lower line 349
22. theorem OAI.PlanarLens.T_tail_gap line 357
23. theorem OAI.PlanarLens.exists_tail_cutoff line 372