OAI/Geometry/Kahler/PinchingCompact.lean

GitHub source file

267 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PinchedHartogs.PlaneAlgebra.HForm line 18
2. instance OAI.PinchedHartogs.PlaneAlgebra.(instance at line 24) line 24
3. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.map_add_left line 30
4. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.map_smul_left line 31
5. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.map_add_right line 32
6. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.map_smul_right line 34
7. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.map_zero_left line 36
8. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.map_zero_right line 38
9. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.map_neg_left line 40
10. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.map_neg_right line 42
11. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.map_sub_left line 44
12. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.map_sub_right line 45
13. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.diag_im line 46
14. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.diag_real line 50
15. def OAI.PinchedHartogs.PlaneAlgebra.HForm.q line 53
16. def OAI.PinchedHartogs.PlaneAlgebra.HForm.area line 55
17. def OAI.PinchedHartogs.PlaneAlgebra.HForm.imag line 57
18. def OAI.PinchedHartogs.PlaneAlgebra.HForm.Nonneg line 59
19. def OAI.PinchedHartogs.PlaneAlgebra.HForm.Pos line 61
20. def OAI.PinchedHartogs.PlaneAlgebra.HForm.Below line 63
21. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.q_zero line 65
22. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.q_smul line 66
23. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.q_add line 69
24. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.q_sub line 72
25. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.nonneg_of_pos line 76
26. def OAI.PinchedHartogs.PlaneAlgebra.HForm.toCore line 82
27. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.gram line 89
28. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.area_nonneg line 98
29. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.q_real_smul line 101
30. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.q_shear line 105
31. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.imag_shear line 111
32. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.q_add_I line 117
33. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.q_sub_I line 120
34. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.imaginary_bound_equal line 123
35. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.imaginary_bound line 137
36. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.area_symm line 174
37. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.q_eq_zero_iff line 178
38. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.dependent_of_area_zero line 187
39. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.imag_eq_zero_of_area_zero line 203
40. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.area_pos line 210
41. def OAI.PinchedHartogs.PlaneAlgebra.HForm.withVertical line 222
42. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.withVertical_q line 228
43. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.withVertical_pos line 232
44. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.area_le_of_bound line 245
45. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.area_ge_of_bound line 270
46. def OAI.PinchedHartogs.PlaneAlgebra.HForm.scale line 281
47. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.scale_q line 287
48. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.scale_imag line 290
49. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.scale_area line 293
50. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.scale_pos line 299
51. def OAI.PinchedHartogs.PlaneAlgebra.verticalImag line 308
52. def OAI.PinchedHartogs.PlaneAlgebra.verticalArea line 310
53. theorem OAI.PinchedHartogs.PlaneAlgebra.vertical_area_eq line 313
54. def OAI.PinchedHartogs.PlaneAlgebra.mixed line 317
55. def OAI.PinchedHartogs.PlaneAlgebra.xi line 320
56. theorem OAI.PinchedHartogs.PlaneAlgebra.xi_q line 322
57. theorem OAI.PinchedHartogs.PlaneAlgebra.augmented_area line 328
58. def OAI.PinchedHartogs.PlaneAlgebra.P line 336
59. theorem OAI.PinchedHartogs.PlaneAlgebra.P_xi line 339
60. theorem OAI.PinchedHartogs.PlaneAlgebra.root_interpolate line 345
61. theorem OAI.PinchedHartogs.PlaneAlgebra.pinch_square_with_xi line 356
62. theorem OAI.PinchedHartogs.PlaneAlgebra.pinch_square_raw line 378
63. theorem OAI.PinchedHartogs.PlaneAlgebra.pinch_square line 402
64. theorem OAI.PinchedHartogs.PlaneAlgebra.pinch_zero_area line 413
65. theorem OAI.PinchedHartogs.PlaneAlgebra.pinch_nonneg line 435
66. theorem OAI.PinchedHartogs.PlaneAlgebra.pinch_equality line 446
67. theorem OAI.PinchedHartogs.PlaneAlgebra.square_gap_core line 516
68. theorem OAI.PinchedHartogs.PlaneAlgebra.sqrt_product_young line 558
69. theorem OAI.PinchedHartogs.PlaneAlgebra.three_error_absorb line 563
70. def OAI.PinchedHartogs.PlaneAlgebra.errorCoefficient line 586
71. def OAI.PinchedHartogs.PlaneAlgebra.thresholdGap line 588
72. def OAI.PinchedHartogs.PlaneAlgebra.pinchingThreshold line 591
73. theorem OAI.PinchedHartogs.PlaneAlgebra.threshold_positive line 597
74. theorem OAI.PinchedHartogs.PlaneAlgebra.large_q_coefficient line 602
75. def OAI.PinchedHartogs.PlaneAlgebra.numerator line 660
76. theorem OAI.PinchedHartogs.PlaneAlgebra.numerator_xi line 665
77. theorem OAI.PinchedHartogs.PlaneAlgebra.delta_bounds line 674
78. theorem OAI.PinchedHartogs.PlaneAlgebra.scaled_square_gap line 691
79. theorem OAI.PinchedHartogs.PlaneAlgebra.numerator_pos_from_bounds line 750
80. def OAI.PinchedHartogs.PlaneAlgebra.PinchAlgebra line 861
81. theorem OAI.PinchedHartogs.PlaneAlgebra.pinch_algebra line 876
82. def OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.form line 909
83. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.form_q line 925
84. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.form_one_q line 928
85. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.hermitian_diag_real line 933
86. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.form_nonneg_iff line 937
87. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.form_sub_q line 950
88. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.form_real_smul_q line 955
89. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.nonneg_difference_iff line 959
90. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.transport_nonneg line 964
91. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.transport_diagonal_nonneg line 974
92. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.transport_real_smul line 979
93. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.diagonal_real_smul line 984
94. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.diagonal_sub_scalar line 991
95. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.scalar_sub_diagonal line 998
96. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.spectral_interval line 1004
97. def OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.horizontalMetric line 1031
98. def OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.mixedMatrix line 1033
99. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.horizontalMetric_hermitian line 1037
100. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.mixedMatrix_hermitian line 1041
101. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.diagonal_metric line 1048
102. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.mixedMatrix_spectral line 1054
103. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.scalar_mixed_bounds line 1097
104. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.scalar_mixed_sharp line 1112
105. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.spectral_comparison line 1155
106. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.spectral_real_scaling line 1170
107. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.form_one_pos line 1176
108. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.mixedMatrix_bounds line 1184
109. theorem OAI.PinchedHartogs.PlaneAlgebra.MatrixAlgebra.actual_numerator_pos line 1231
110. abbrev OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.Quad line 1258
111. abbrev OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.Tensor line 1259
112. structure OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.Symmetries line 1261
113. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.eval line 1266
114. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H line 1270
115. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.Xi line 1273
116. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.xiContract line 1275
117. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.swapHol line 1278
118. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.swapAnti line 1284
119. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.swapConj line 1290
120. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.eval_hol line 1296
121. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.eval_anti line 1305
122. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.eval_conj line 1314
123. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.xiContract_expand line 1326
124. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H_xi line 1336
125. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.componentNorm line 1343
126. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.norm_component_le line 1346
127. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H_abs_bound line 1357
128. abbrev OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.Index line 1366
129. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.lift line 1368
130. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.horizontalCount line 1370
131. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.Supported line 1374
132. abbrev OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.euclidean line 1377
133. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.xi_horizontal_norm line 1379
134. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.xi_horizontal_bound line 1386
135. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.xi_mixed_bound line 1400
136. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.xi_reverse line 1413
137. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.xi_mixed_reverse_bound line 1417
138. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.xi_pair_four line 1424
139. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.xi_pair_three line 1439
140. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.four_error line 1464
141. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.three_error line 1488
142. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.S line 1517
143. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.productTensor line 1520
144. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.eval_product line 1524
145. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.eval_add line 1541
146. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.eval_permAnti line 1546
147. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.eval_S line 1554
148. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H_S line 1561
149. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H_add line 1574
150. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H_sub line 1579
151. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H_smul line 1584
152. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.block line 1594
153. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.block_hermitian line 1600
154. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.block_pair line 1606
155. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.horizontal_area line 1613
156. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.horizontal_imag line 1619
157. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H_horizontal line 1625
158. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H_augmented line 1631
159. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H_vertical line 1647
160. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.curvatureModel line 1652
161. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.negative_numerator line 1658
162. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.curvatureModel_negative line 1670
163. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pinch_positivity line 1708
164. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pullTensor line 1734
165. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pullVector line 1737
166. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pullMatrix line 1739
167. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.eval_pull line 1742
168. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H_pull line 1750
169. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pull_add line 1755
170. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pull_sub line 1761
171. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pull_smul line 1767
172. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pull_comp line 1774
173. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pull_one line 1781
174. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pull_symmetries line 1786
175. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pull_S line 1803
176. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.horizontalScale line 1811
177. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.horizontal_product line 1813
178. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pull_supported line 1819
179. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pull_horizontal_matrix line 1828
180. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.horizontal_pull_lift line 1834
181. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.horizontal_independent line 1839
182. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.mixedTensor line 1860
183. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.mixedTensor_smul line 1863
184. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pull_mixedTensor line 1869
185. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.S_smul line 1874
186. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.block_horizontal_smul line 1880
187. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactG line 1885
188. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactD line 1888
189. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactCurvature line 1891
190. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.form_pos_iff line 1896
191. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.G_posdef line 1911
192. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.inv_real_smul line 1933
193. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactG_eq line 1939
194. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactD_eq line 1944
195. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pull_model line 1955
196. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.componentNorm_smul line 1976
197. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.supported_smul line 1982
198. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.symmetries_smul line 1987
199. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compact_scalars line 2006
200. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.componentNorm_eq_zero line 2032
201. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.liftEquiv line 2037
202. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.independent_lift line 2045
203. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.block_pos line 2056
204. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactCurvature_negative line 2073
205. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.isClosed_setOf_forall line 2155
206. abbrev OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.BaseMatrix line 2159
207. abbrev OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.FullVector line 2160
208. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pairValue line 2162
209. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.qValue line 2165
210. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuous_pairValue line 2168
211. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuous_qValue line 2173
212. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.matrix_entry_bound line 2178
213. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.matrixSet line 2200
214. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.matrixSet_closed line 2203
215. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.matrixSet_compact line 2212
216. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pairSet line 2227
217. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pairSet_closed line 2230
218. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.qValue_one line 2235
219. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.norm_le_of_q_one line 2238
220. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pairSet_compact line 2247
221. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.independent_pairSet line 2253
222. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuous_componentNorm line 2286
223. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.norm_le_componentNorm line 2290
224. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.symmetries_iff line 2302
225. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.symmetries_closed line 2308
226. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.supported_closed line 2322
227. abbrev OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.CompactData line 2341
228. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.dataSet line 2343
229. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.dataSet_closed line 2350
230. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.dataSet_compact line 2363
231. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactG_hermitian line 2384
232. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactG_pos line 2388
233. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuous_block line 2420
234. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuous_S line 2427
235. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuous_mixedTensor line 2431
236. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuous_H line 2436
237. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuousAt_matrix_inverse line 2441
238. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuous_compactG line 2448
239. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuousAt_compactD line 2453
240. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuousAt_compactCurvature line 2473
241. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.metricArea line 2491
242. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.continuous_metricArea line 2494
243. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactQuotient line 2505
244. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.metricArea_pos line 2509
245. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactQuotient_negative line 2519
246. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactMetric_continuous line 2546
247. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactArea_continuous line 2551
248. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactNumerator_continuousAt line 2558
249. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactQuotient_continuous line 2568
250. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compact_uniform_pinching line 2577
251. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.real_pair_shear_scale line 2602
252. theorem OAI.PinchedHartogs.PlaneAlgebra.HForm.area_shear_scale line 2610
253. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.S_symmetries line 2622
254. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.symmetries_add line 2638
255. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.symmetries_sub line 2645
256. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.mixed_symmetries line 2652
257. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactD_hermitian line 2656
258. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compactCurvature_symmetries line 2662
259. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.Xi_shear_scale line 2674
260. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.H_shear_scale line 2681
261. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.normalization line 2696
262. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.compact_uniform_all_planes line 2732
263. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.pairValue_pull line 2768
264. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.metricArea_pull line 2780
265. def OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.horizontalPullEquiv line 2787
266. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.horizontalPull_independent line 2803
267. theorem OAI.PinchedHartogs.PlaneAlgebra.TensorAlgebra.curvatureModel_uniform_pinching line 2814