OAI/Geometry/ConjugatePoints/Quotient.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThreeManifold.QuotientConstruction.productAction line 20
2. lemma OAI.ThreeManifold.QuotientConstruction.product_cover line 30
3. lemma OAI.ThreeManifold.QuotientConstruction.cover_precomp line 59
4. lemma OAI.ThreeManifold.QuotientConstruction.lifts_eventuallyEq line 99
5. lemma OAI.ThreeManifold.QuotientConstruction.cover_lift_eventuallyEq_action line 111
6. def OAI.ThreeManifold.QuotientConstruction.quotientCharts line 137
7. lemma OAI.ThreeManifold.QuotientConstruction.transition_eventuallyEq_action line 146
8. lemma OAI.ThreeManifold.QuotientConstruction.quotient_isManifold line 163
9. lemma OAI.ThreeManifold.QuotientConstruction.quotient_projection_smooth line 187
10. def OAI.ThreeManifold.QuotientConstruction.manifoldCharts line 215
11. lemma OAI.ThreeManifold.QuotientConstruction.manifold_quotient_isManifold line 218
12. lemma OAI.ThreeManifold.QuotientConstruction.manifold_quotient_projection_smooth line 263
13. lemma OAI.ThreeManifold.QuotientConstruction.chosen_lift_smoothAt line 288
14. lemma OAI.ThreeManifold.QuotientConstruction.local_lift_smoothAt line 311
15. def OAI.ThreeManifold.HyperbolicCore.phi line 345
16. def OAI.ThreeManifold.HyperbolicCore.psi line 346
17. def OAI.ThreeManifold.HyperbolicCore.Γ line 347
18. def OAI.ThreeManifold.HyperbolicCore.red line 349
19. def OAI.ThreeManifold.HyperbolicCore.qset line 352
20. def OAI.ThreeManifold.HyperbolicCore.Q line 356
21. def OAI.ThreeManifold.HyperbolicCore.pset line 369
22. def OAI.ThreeManifold.HyperbolicCore.P line 371
23. theorem OAI.ThreeManifold.HyperbolicCore.red_two_mem line 384
24. theorem OAI.ThreeManifold.HyperbolicCore.red_three_mem line 394
25. lemma OAI.ThreeManifold.HyperbolicCore.P_trace_zero line 404
26. lemma OAI.ThreeManifold.HyperbolicCore.Q_trace_one line 412
27. lemma OAI.ThreeManifold.HyperbolicCore.Q_trace_neg_one line 419
28. lemma OAI.ThreeManifold.HyperbolicCore.det_congruence_trace line 426
29. lemma OAI.ThreeManifold.HyperbolicCore.red_one_trace line 439
30. theorem OAI.ThreeManifold.HyperbolicCore.trace_not_small line 453
31. lemma OAI.ThreeManifold.HyperbolicCore.mapGL_det line 482
32. theorem OAI.ThreeManifold.HyperbolicCore.not_elliptic line 489
33. theorem OAI.ThreeManifold.HyperbolicCore.fixed_point_trivial line 504
34. instance OAI.ThreeManifold.HyperbolicCore.integer_proper line 520
35. def OAI.ThreeManifold.HyperbolicCore.effective line 530
36. def OAI.ThreeManifold.HyperbolicCore.effect line 532
37. lemma OAI.ThreeManifold.HyperbolicCore.effect_surjective line 534
38. lemma OAI.ThreeManifold.HyperbolicCore.effect_smul line 537
39. instance OAI.ThreeManifold.HyperbolicCore.effective_cancel line 539
40. instance OAI.ThreeManifold.HyperbolicCore.effective_continuous line 548
41. instance OAI.ThreeManifold.HyperbolicCore.effective_proper line 554
42. def OAI.ThreeManifold.HyperbolicCore.Surface line 563
43. instance OAI.ThreeManifold.HyperbolicCore.(instance at line 564) line 564
44. def OAI.ThreeManifold.HyperbolicCore.projection line 566
45. lemma OAI.ThreeManifold.HyperbolicCore.projection_cover line 568
46. instance OAI.ThreeManifold.HyperbolicCore.halfplane_real_manifold line 578
47. lemma OAI.ThreeManifold.HyperbolicCore.action_smooth line 581
48. lemma OAI.ThreeManifold.HyperbolicCore.effective_smooth line 591
49. def OAI.ThreeManifold.HyperbolicCore.sectionMap line 596
50. lemma OAI.ThreeManifold.HyperbolicCore.sectionMap_rightInverse line 597
51. instance OAI.ThreeManifold.HyperbolicCore.surfaceCharts line 600
52. instance OAI.ThreeManifold.HyperbolicCore.surfaceSmooth line 602
53. lemma OAI.ThreeManifold.HyperbolicCore.projection_smooth line 605
54. instance OAI.ThreeManifold.HyperbolicCore.(instance at line 608) line 608
55. instance OAI.ThreeManifold.HyperbolicCore.(instance at line 609) line 609
56. instance OAI.ThreeManifold.HyperbolicCore.(instance at line 610) line 610
57. instance OAI.ThreeManifold.HyperbolicCore.surfaceT2 line 612
58. instance OAI.ThreeManifold.HyperbolicCore.surfaceSecondCountable line 614
59. instance OAI.ThreeManifold.HyperbolicCore.surfaceConnected line 616
60. lemma OAI.ThreeManifold.HyperbolicCore.phi_mem line 627
61. lemma OAI.ThreeManifold.HyperbolicCore.psi_mem line 628
62. lemma OAI.ThreeManifold.HyperbolicCore.neg_one_mem line 629
63. lemma OAI.ThreeManifold.HyperbolicCore.conj_preserves line 631
64. lemma OAI.ThreeManifold.HyperbolicCore.S_preserves line 645
65. lemma OAI.ThreeManifold.HyperbolicCore.Sinv_preserves line 652
66. lemma OAI.ThreeManifold.HyperbolicCore.T_preserves line 659
67. lemma OAI.ThreeManifold.HyperbolicCore.Tinv_preserves line 666
68. lemma OAI.ThreeManifold.HyperbolicCore.normalizer_of_preserves line 673
69. instance OAI.ThreeManifold.HyperbolicCore.gamma_normal line 683
70. lemma OAI.ThreeManifold.HyperbolicCore.peripheral_matrix line 693
71. lemma OAI.ThreeManifold.HyperbolicCore.T_six_mem line 695
72. lemma OAI.ThreeManifold.HyperbolicCore.S_coset_relation line 701
73. def OAI.ThreeManifold.HyperbolicCore.qmap line 703
74. lemma OAI.ThreeManifold.HyperbolicCore.qmap_phi line 705
75. lemma OAI.ThreeManifold.HyperbolicCore.qmap_psi line 706
76. lemma OAI.ThreeManifold.HyperbolicCore.qmap_neg_one line 707
77. lemma OAI.ThreeManifold.HyperbolicCore.qmap_S line 709
78. lemma OAI.ThreeManifold.HyperbolicCore.qmap_T_six line 713
79. lemma OAI.ThreeManifold.HyperbolicCore.qmap_cyclic line 717
80. lemma OAI.ThreeManifold.HyperbolicCore.qmap_representative line 730
81. theorem OAI.ThreeManifold.HyperbolicCore.coset_representative line 746
82. lemma OAI.ThreeManifold.HyperbolicCore.T_zpow_mem_iff line 758
83. lemma OAI.ThreeManifold.HyperbolicCore.projection_smul line 786
84. lemma OAI.ThreeManifold.HyperbolicCore.projection_eq_iff line 790
85. lemma OAI.ThreeManifold.HyperbolicCore.bottomLeft_eq_zero_of_high line 800
86. lemma OAI.ThreeManifold.HyperbolicCore.matrix_eq_T_zpow_of_c_eq_zero line 816
87. theorem OAI.ThreeManifold.HyperbolicCore.projection_high_eq_iff line 828
88. def OAI.ThreeManifold.HyperbolicCore.cusp line 857
89. lemma OAI.ThreeManifold.HyperbolicCore.cusp_open line 859
90. theorem OAI.ThreeManifold.HyperbolicCore.cusp_complement_compact line 862
91. def OAI.ThreeManifold.HyperbolicCore.highCoordinates line 897
92. def OAI.ThreeManifold.HyperbolicCore.highProjection line 912
93. lemma OAI.ThreeManifold.HyperbolicCore.highProjection_openQuotient line 915
94. def OAI.ThreeManifold.HyperbolicCore.highCylinderProjection line 934
95. lemma OAI.ThreeManifold.HyperbolicCore.highCylinderProjection_openQuotient line 937
96. lemma OAI.ThreeManifold.HyperbolicCore.circle_six_eq_iff line 943
97. lemma OAI.ThreeManifold.HyperbolicCore.highProjection_sameFibers line 949
98. def OAI.ThreeManifold.HyperbolicCore.fiberHomeomorph line 974
99. lemma OAI.ThreeManifold.HyperbolicCore.fiberHomeomorph_apply line 1000
100. def OAI.ThreeManifold.HyperbolicCore.cuspCoordinates line 1006
101. lemma OAI.ThreeManifold.HyperbolicCore.cuspCoordinates_apply line 1011
102. lemma OAI.ThreeManifold.HyperbolicCore.integer_action_isometry line 1020
103. def OAI.ThreeManifold.HyperbolicCore.maxIm line 1023
104. lemma OAI.ThreeManifold.HyperbolicCore.maxIm_pos line 1024
105. lemma OAI.ThreeManifold.HyperbolicCore.im_smul_le_maxIm line 1025
106. lemma OAI.ThreeManifold.HyperbolicCore.im_le_maxIm line 1027
107. lemma OAI.ThreeManifold.HyperbolicCore.maxIm_smul line 1030
108. def OAI.ThreeManifold.HyperbolicCore.logMaxIm line 1037
109. lemma OAI.ThreeManifold.HyperbolicCore.logMaxIm_smul line 1038
110. lemma OAI.ThreeManifold.HyperbolicCore.logMaxIm_sub_le_dist line 1042
111. lemma OAI.ThreeManifold.HyperbolicCore.logMaxIm_lipschitz line 1052
112. def OAI.ThreeManifold.HyperbolicCore.height line 1059
113. lemma OAI.ThreeManifold.HyperbolicCore.height_projection line 1061
114. lemma OAI.ThreeManifold.HyperbolicCore.height_continuous line 1067
115. lemma OAI.ThreeManifold.HyperbolicCore.maxIm_eq_im_of_high line 1073
116. lemma OAI.ThreeManifold.HyperbolicCore.height_projection_high line 1084
117. lemma OAI.ThreeManifold.HyperbolicCore.mem_cusp_iff_height line 1088
118. lemma OAI.ThreeManifold.HyperbolicCore.height_sublevel_compact line 1107
119. def OAI.ThreeManifold.HyperbolicCore.OpenCore line 1115
120. instance OAI.ThreeManifold.HyperbolicCore.(instance at line 1116) line 1116
121. lemma OAI.ThreeManifold.HyperbolicCore.openCore_open line 1119
122. lemma OAI.ThreeManifold.HyperbolicCore.compact_core_slice line 1122
123. lemma OAI.ThreeManifold.HyperbolicCore.height_cuspCoordinates line 1134
124. def OAI.ThreeManifold.HyperbolicCore.clipCusp line 1142
125. lemma OAI.ThreeManifold.HyperbolicCore.clipCusp_of_mem line 1151
126. lemma OAI.ThreeManifold.HyperbolicCore.clipCusp_eq_self line 1160
127. lemma OAI.ThreeManifold.HyperbolicCore.clipCusp_height_le line 1172
128. lemma OAI.ThreeManifold.HyperbolicCore.clipCusp_continuous_on_cusp line 1183
129. lemma OAI.ThreeManifold.HyperbolicCore.clipCusp_continuous line 1192
130. lemma OAI.ThreeManifold.HyperbolicCore.range_clipCusp line 1207
131. lemma OAI.ThreeManifold.HyperbolicCore.height_sublevel_connected line 1214
132. lemma OAI.ThreeManifold.HyperbolicCore.openCore_preconnected line 1220
133. lemma OAI.ThreeManifold.HyperbolicCore.openCore_nonempty line 1238
134. lemma OAI.ThreeManifold.HyperbolicCore.openCore_connected line 1245