OAI/Geometry/PolarProducts/LensArea.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarLens.D line 37
2. def OAI.PlanarLens.g line 39
3. theorem OAI.PlanarLens.g_F line 41
4. theorem OAI.PlanarLens.F_g line 44
5. theorem OAI.PlanarLens.norm_g_lt line 47
6. theorem OAI.PlanarLens.zero_mem_D line 51
7. theorem OAI.PlanarLens.g_zero line 53
8. theorem OAI.PlanarLens.g_eq_zero_iff line 56
9. theorem OAI.PlanarLens.deriv_F_ne_zero line 62
10. theorem OAI.PlanarLens.analyticOnNhd_g line 68
11. theorem OAI.PlanarLens.isOpen_D line 77
12. theorem OAI.PlanarLens.isBounded_D line 86
13. theorem OAI.PlanarLens.continuousOn_g line 90
14. theorem OAI.PlanarLens.g_injOn line 92
15. theorem OAI.PlanarLens.deriv_g_F line 96
16. theorem OAI.PlanarLens.deriv_g_ne_zero line 109
17. theorem OAI.PlanarLens.re_g_pos line 113
18. def OAI.PlanarLens.T line 131
19. theorem OAI.PlanarLens.F_imaginary line 133
20. theorem OAI.PlanarLens.T_zero line 136
21. theorem OAI.PlanarLens.T_neg line 138
22. theorem OAI.PlanarLens.summable_odd_sq line 140
23. theorem OAI.PlanarLens.tsum_odd_sq line 145
24. theorem OAI.PlanarLens.F_I line 164
25. theorem OAI.PlanarLens.T_one line 178
26. theorem OAI.PlanarLens.continuousOn_T line 180
27. theorem OAI.PlanarLens.hasDerivAt_T line 187
28. theorem OAI.PlanarLens.strictMonoOn_T line 194
29. theorem OAI.PlanarLens.T_pos line 203
30. theorem OAI.PlanarLens.T_lt_one line 207
31. theorem OAI.PlanarLens.exists_T_eq line 211
32. def OAI.PlanarLens.A line 233
33. theorem OAI.PlanarLens.A_pos line 235
34. theorem OAI.PlanarLens.hasDerivAt_horizontal_g line 242
35. theorem OAI.PlanarLens.horizontal_normSq_deriv line 249
36. theorem OAI.PlanarLens.horizontal_normSq_deriv_pos line 262
37. theorem OAI.PlanarLens.horizontal_segment_mem line 269
38. theorem OAI.PlanarLens.neg_conj_mem_D line 337
39. theorem OAI.PlanarLens.g_neg_conj line 342
40. theorem OAI.PlanarLens.conj_mem_D line 348
41. theorem OAI.PlanarLens.g_conj line 352
42. theorem OAI.PlanarLens.horizontal_segment_mem_signed line 357
43. theorem OAI.PlanarLens.axis_mem_D line 372
44. theorem OAI.PlanarLens.g_axis_re_zero line 375
45. theorem OAI.PlanarLens.axis_image line 383
46. theorem OAI.PlanarLens.im_mem_Ioo line 397
47. theorem OAI.PlanarLens.imaginary_mem_D line 405
48. theorem OAI.PlanarLens.horizontal_radius_strictMono line 410
49. theorem OAI.PlanarLens.T_norm_g_axis line 424
50. theorem OAI.PlanarLens.vertical_gap_pos line 438