OAI/Geometry/PolarProducts/LensMap.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarLens.term line 36
2. def OAI.PlanarLens.termDeriv line 38
3. def OAI.PlanarLens.F line 40
4. theorem OAI.PlanarLens.hasDerivAt_term line 42
5. theorem OAI.PlanarLens.term_zero line 51
6. theorem OAI.PlanarLens.F_zero line 53
7. theorem OAI.PlanarLens.norm_termDeriv_le line 55
8. theorem OAI.PlanarLens.summable_termDeriv line 67
9. theorem OAI.PlanarLens.hasDerivAt_F line 71
10. theorem OAI.PlanarLens.analyticOnNhd_F line 85
11. theorem OAI.PlanarLens.mul_deriv_F line 90
12. theorem OAI.PlanarLens.norm_term_le line 103
13. theorem OAI.PlanarLens.summable_bound line 116
14. theorem OAI.PlanarLens.summable_term line 120
15. theorem OAI.PlanarLens.continuousOn_F_closedBall line 123
16. theorem OAI.PlanarLens.F_norm_le line 130
17. theorem OAI.PlanarLens.F_neg line 138
18. theorem OAI.PlanarLens.F_conj line 146
19. def OAI.PlanarLens.cayley line 153
20. theorem OAI.PlanarLens.cayley_re line 155
21. theorem OAI.PlanarLens.cayley_im line 161
22. theorem OAI.PlanarLens.cayley_re_pos line 167
23. theorem OAI.PlanarLens.arctan_re_eq line 176
24. theorem OAI.PlanarLens.re_mul_deriv_F line 197
25. theorem OAI.PlanarLens.norm_one_add_mul_I_sq line 210
26. theorem OAI.PlanarLens.norm_one_sub_mul_I_sq line 215
27. theorem OAI.PlanarLens.one_add_mul_I_ne_zero line 220
28. theorem OAI.PlanarLens.one_sub_mul_I_ne_zero line 227
29. theorem OAI.PlanarLens.arctan_im_eq line 231
30. theorem OAI.PlanarLens.arctan_im_pos line 239
31. theorem OAI.PlanarLens.arctan_im_neg line 251
32. theorem OAI.PlanarLens.arctan_im_mul_nonneg line 262
33. theorem OAI.PlanarLens.arctan_re_mul_nonneg line 269
34. theorem OAI.PlanarLens.arctan_div_re_pos line 282
35. theorem OAI.PlanarLens.deriv_F_zero line 307
36. theorem OAI.PlanarLens.deriv_F_re_pos line 317
37. theorem OAI.PlanarLens.F_injOn line 328
38. theorem OAI.PlanarLens.re_F_imaginary line 359
39. theorem OAI.PlanarLens.re_F_pos line 367
40. theorem OAI.PlanarLens.re_F_neg line 393
41. theorem OAI.PlanarLens.re_F_eq_zero line 397