OAI/Geometry/PrescribedPotential/AnalyticSupport.lean

GitHub source file

236 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ProjectiveKaehler.compactIntegral line 19
2. abbrev OAI.ProjectiveKaehler.Angle line 39
3. def OAI.ProjectiveKaehler.angleMeasure line 41
4. instance OAI.ProjectiveKaehler.(instance at line 43) line 43
5. abbrev OAI.ProjectiveKaehler.Boundary line 51
6. def OAI.ProjectiveKaehler.boundaryCons line 53
7. def OAI.ProjectiveKaehler.integrateFirst line 64
8. def OAI.ProjectiveKaehler.boundaryIntegral line 97
9. theorem OAI.ProjectiveKaehler.boundaryIntegral_zero line 102
10. theorem OAI.ProjectiveKaehler.boundaryIntegral_succ line 105
11. def OAI.ProjectiveKaehler.boundaryPoint line 110
12. def OAI.ProjectiveKaehler.denominator line 119
13. lemma OAI.ProjectiveKaehler.analyticAt_denominator line 125
14. lemma OAI.ProjectiveKaehler.isUnit_denominator line 139
15. lemma OAI.ProjectiveKaehler.analyticAt_inverseDenominator line 150
16. lemma OAI.ProjectiveKaehler.inverseDenominator_apply line 158
17. lemma OAI.ProjectiveKaehler.boundaryPoint_mem_closedBall line 166
18. def OAI.ProjectiveKaehler.boundaryValue line 172
19. def OAI.ProjectiveKaehler.boundarySpeed line 178
20. def OAI.ProjectiveKaehler.cauchyTransform line 183
21. lemma OAI.ProjectiveKaehler.analyticAt_cauchyTransform line 187
22. abbrev OAI.ProjectiveKaehler.circleKernel line 199
23. lemma OAI.ProjectiveKaehler.cauchyIntegrand_apply line 202
24. lemma OAI.ProjectiveKaehler.circleCauchy line 210
25. lemma OAI.ProjectiveKaehler.differentiable_cons_left line 220
26. lemma OAI.ProjectiveKaehler.differentiable_cons_right line 228
27. lemma OAI.ProjectiveKaehler.cons_mem_closedBall line 236
28. lemma OAI.ProjectiveKaehler.tail_mem_ball line 248
29. lemma OAI.ProjectiveKaehler.boundaryPoint_cons line 255
30. lemma OAI.ProjectiveKaehler.boundaryIntegral_cauchy line 264
31. lemma OAI.ProjectiveKaehler.cauchyTransform_eq line 310
32. lemma OAI.ProjectiveKaehler.analyticAt_of_differentiableOn_closedBall line 319
33. theorem OAI.ProjectiveKaehler.analyticOnNhd_of_differentiableOn line 333
34. theorem OAI.ProjectiveKaehler.analyticOnNhd_pi_of_differentiableOn line 342
35. theorem OAI.ProjectiveKaehler.contDiffOn_real_pi_of_differentiableOn line 352
36. def OAI.ProjectiveKaehler.mass line 371
37. lemma OAI.ProjectiveKaehler.mass_ne_zero line 373
38. lemma OAI.ProjectiveKaehler.mass_pos line 376
39. lemma OAI.ProjectiveKaehler.star_mass line 379
40. def OAI.ProjectiveKaehler.horizontal line 383
41. lemma OAI.ProjectiveKaehler.horizontal_mulVec line 386
42. lemma OAI.ProjectiveKaehler.horizontal_mulVec_eq_zero_iff line 390
43. lemma OAI.ProjectiveKaehler.horizontal_self line 394
44. lemma OAI.ProjectiveKaehler.horizontal_eq_conjTranspose line 399
45. lemma OAI.ProjectiveKaehler.horizontal_idempotent line 402
46. def OAI.ProjectiveKaehler.fsMatrix line 414
47. lemma OAI.ProjectiveKaehler.fsMatrix_posDef line 418
48. lemma OAI.ProjectiveKaehler.fsMatrix_eq line 423
49. lemma OAI.ProjectiveKaehler.mass_smul line 431
50. lemma OAI.ProjectiveKaehler.horizontal_smul line 436
51. lemma OAI.ProjectiveKaehler.horizontal_gauge line 444
52. lemma OAI.ProjectiveKaehler.fsMatrix_gauge line 452
53. lemma OAI.ProjectiveKaehler.fsMatrix_comp line 461
54. lemma OAI.ProjectiveKaehler.fsMatrix_pair line 469
55. def OAI.ProjectiveKaehler.jacobianMatrix line 480
56. lemma OAI.ProjectiveKaehler.jacobianMatrix_mulVec line 483
57. lemma OAI.ProjectiveKaehler.normalized_derivative line 487
58. lemma OAI.ProjectiveKaehler.fsMatrix_posDef_of_immersion line 509
59. abbrev OAI.Anticanonical.Coordinates line 535
60. def OAI.Anticanonical.coordinateOverlap line 538
61. structure OAI.Anticanonical.ComplexAtlas line 544
62. def OAI.Anticanonical.ComplexAtlas.transition line 556
63. def OAI.Anticanonical.ComplexAtlas.jacobian line 561
64. structure OAI.Anticanonical.ComplexAtlas.ProjectiveEmbedding line 567
65. lemma OAI.Anticanonical.ComplexAtlas.isOpen_coordinateOverlap line 588
66. lemma OAI.Anticanonical.ComplexAtlas.coordinate_mem_overlap line 592
67. lemma OAI.Anticanonical.ComplexAtlas.transition_at line 599
68. lemma OAI.Anticanonical.ComplexAtlas.differentiableAt_transition line 603
69. def OAI.Anticanonical.ComplexAtlas.derivativeMatrix line 617
70. def OAI.Anticanonical.ComplexAtlas.fundamentalForm line 622
71. structure OAI.Anticanonical.ComplexAtlas.KaehlerMetric line 628
72. lemma OAI.ProjectiveKaehler.smooth_conj line 648
73. lemma OAI.ProjectiveKaehler.smooth_mass line 652
74. lemma OAI.ProjectiveKaehler.smooth_horizontal line 659
75. lemma OAI.ProjectiveKaehler.smooth_matrix_mul line 670
76. lemma OAI.ProjectiveKaehler.smooth_conjTranspose line 684
77. lemma OAI.ProjectiveKaehler.smooth_fsMatrix line 692
78. lemma OAI.ProjectiveKaehler.smooth_jacobianMatrix line 700
79. def OAI.Anticanonical.ComplexAtlas.ProjectiveEmbedding.backgroundMatrix line 721
80. lemma OAI.Anticanonical.ComplexAtlas.ProjectiveEmbedding.backgroundMatrix_smooth line 725
81. lemma OAI.Anticanonical.ComplexAtlas.ProjectiveEmbedding.backgroundMatrix_positive line 732
82. lemma OAI.ProjectiveKaehler.jacobianMatrix_comp line 745
83. lemma OAI.ProjectiveKaehler.jacobianMatrix_smul line 753
84. lemma OAI.ProjectiveKaehler.fsMatrix_eq_of_eventually_proportional line 765
85. lemma OAI.Anticanonical.ComplexAtlas.ProjectiveEmbedding.backgroundMatrix_compatibility line 804
86. def OAI.ProjectiveKaehler.Closedness.pair line 847
87. lemma OAI.ProjectiveKaehler.Closedness.star_pair line 849
88. lemma OAI.ProjectiveKaehler.Closedness.pair_self_ne_zero line 852
89. lemma OAI.ProjectiveKaehler.Closedness.smooth_pair line 855
90. lemma OAI.ProjectiveKaehler.Closedness.fderiv_pair_apply line 864
91. lemma OAI.ProjectiveKaehler.Closedness.fderiv_eval_derivative line 887
92. lemma OAI.ProjectiveKaehler.Closedness.second_derivative_symmetric line 894
93. def OAI.ProjectiveKaehler.Closedness.beta line 902
94. lemma OAI.ProjectiveKaehler.Closedness.smooth_beta line 905
95. lemma OAI.ProjectiveKaehler.Closedness.fderiv_inv_complex_apply line 911
96. lemma OAI.ProjectiveKaehler.Closedness.fderiv_im_apply line 919
97. lemma OAI.ProjectiveKaehler.Closedness.fderiv_beta line 925
98. lemma OAI.ProjectiveKaehler.Closedness.anti_beta_algebra line 955
99. def OAI.ProjectiveKaehler.Closedness.omega line 971
100. lemma OAI.ProjectiveKaehler.Closedness.beta_antisym line 976
101. lemma OAI.ProjectiveKaehler.Closedness.cyclic_antisym_derivative line 988
102. lemma OAI.ProjectiveKaehler.Closedness.smooth_omega line 1001
103. lemma OAI.ProjectiveKaehler.Closedness.omega_closed line 1012
104. lemma OAI.ProjectiveKaehler.fundamentalForm_fs_eq_omega line 1039
105. lemma OAI.Anticanonical.ComplexAtlas.ProjectiveEmbedding.backgroundMatrix_closed line 1057
106. def OAI.Anticanonical.ComplexAtlas.ProjectiveEmbedding.backgroundKaehlerMetric line 1077
107. theorem OAI.Anticanonical.ComplexAtlas.ProjectiveEmbedding.nonemptyKaehlerMetric line 1084
108. def OAI.Anticanonical.SourceSmooth.levi line 1098
109. structure OAI.Anticanonical.SourceSmooth.SemipositiveAnticanonicalMetric line 1103
110. structure OAI.Anticanonical.SourceSmooth.KaehlerMetric line 1113
111. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumeCoefficient line 1127
112. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.ricciPotential line 1130
113. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.ricciQuadratic line 1133
114. def OAI.Anticanonical.SourceSmooth.PrescribedRicci line 1139
115. def OAI.Anticanonical.SourceSmooth.projectiveBackground line 1155
116. abbrev OAI.PotentialKaehler.V line 1172
117. abbrev OAI.PotentialKaehler.RealBilinear line 1173
118. def OAI.PotentialKaehler.hermitianPart line 1177
119. lemma OAI.PotentialKaehler.complex_smul_decompose line 1181
120. lemma OAI.PotentialKaehler.hermitianPart_add_left line 1187
121. lemma OAI.PotentialKaehler.hermitianPart_add_right line 1191
122. lemma OAI.PotentialKaehler.hermitianPart_real_smul_left line 1195
123. lemma OAI.PotentialKaehler.hermitianPart_real_smul_right line 1199
124. lemma OAI.PotentialKaehler.hermitianPart_I_left line 1203
125. lemma OAI.PotentialKaehler.hermitianPart_I_right line 1207
126. lemma OAI.PotentialKaehler.hermitianPart_smul_left line 1211
127. lemma OAI.PotentialKaehler.hermitianPart_smul_right line 1217
128. def OAI.PotentialKaehler.hermitianPartForm line 1225
129. lemma OAI.PotentialKaehler.hermitianPart_star line 1239
130. def OAI.PotentialKaehler.hermitianPartMatrix line 1245
131. lemma OAI.PotentialKaehler.hermitianPartMatrix_apply line 1248
132. lemma OAI.PotentialKaehler.hermitianPartMatrix_pair line 1252
133. lemma OAI.PotentialKaehler.hermitianPartMatrix_hermitian line 1257
134. def OAI.PotentialKaehler.potentialMatrix line 1263
135. lemma OAI.PotentialKaehler.potentialMatrix_hermitian line 1266
136. lemma OAI.PotentialKaehler.smooth_hermitianPart line 1271
137. lemma OAI.PotentialKaehler.potentialMatrix_smooth line 1282
138. lemma OAI.PotentialKaehler.fderiv_eval_derivative line 1296
139. lemma OAI.PotentialKaehler.second_derivative_symmetric line 1302
140. lemma OAI.PotentialKaehler.cyclic_antisym_derivative line 1309
141. def OAI.PotentialKaehler.potentialPrimitive line 1324
142. def OAI.PotentialKaehler.potentialForm line 1327
143. lemma OAI.PotentialKaehler.potentialPrimitive_smooth line 1330
144. lemma OAI.PotentialKaehler.potentialPrimitive_derivative line 1335
145. lemma OAI.PotentialKaehler.potentialPrimitive_antisym line 1351
146. lemma OAI.PotentialKaehler.potentialMatrix_closed line 1360
147. lemma OAI.PotentialKaehler.eventually_differentiableAt line 1379
148. lemma OAI.PotentialKaehler.second_derivative_comp line 1386
149. lemma OAI.PotentialKaehler.fderiv_complex_smul line 1412
150. lemma OAI.PotentialKaehler.second_derivative_complex_smul_right line 1418
151. lemma OAI.PotentialKaehler.second_derivative_complex_smul_left line 1436
152. lemma OAI.PotentialKaehler.hermitianPart_comp line 1448
153. lemma OAI.PotentialKaehler.matrix_pair_pullback line 1461
154. lemma OAI.PotentialKaehler.matrix_eq_of_pair line 1466
155. lemma OAI.PotentialKaehler.potentialMatrix_congr line 1471
156. lemma OAI.PotentialKaehler.potentialMatrix_comp line 1476
157. structure OAI.Anticanonical.SourceSmooth.SmoothRealFunction line 1497
158. def OAI.Anticanonical.SourceSmooth.SmoothRealFunction.localExpression line 1503
159. def OAI.Anticanonical.SourceSmooth.SmoothRealFunction.hessian line 1507
160. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.hessian_smooth line 1510
161. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.hessian_hermitian line 1516
162. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.hessian_compatibility line 1521
163. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.hessian_closed line 1542
164. lemma OAI.Anticanonical.SourceSmooth.fundamentalForm_add line 1551
165. lemma OAI.Anticanonical.SourceSmooth.fundamentalForm_smooth line 1556
166. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.PositivePotential line 1572
167. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.deform line 1577
168. lemma OAI.MongeAmpere.hasDerivAt_det_one_add_smul line 1607
169. lemma OAI.MongeAmpere.hasDerivAt_det_add_smul line 1613
170. lemma OAI.MongeAmpere.hasDerivAt_logdet_add_smul line 1628
171. lemma OAI.MongeAmpere.linearized_symbol_pos line 1640
172. def OAI.Anticanonical.SourceSmooth.SmoothRealFunction.constant line 1655
173. def OAI.Anticanonical.SourceSmooth.SmoothRealFunction.realSMul line 1659
174. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.hessian_constant line 1663
175. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.hessian_realSMul line 1669
176. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.linearizedMongeAmpere line 1688
177. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.mongeAmpere_directional_derivative line 1693
178. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.linearizedMongeAmpere_constant line 1702
179. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.linearizedMongeAmpere_not_injective line 1709
180. lemma OAI.EllipticKernel.second_deriv_nonpos_at_localMax line 1725
181. lemma OAI.EllipticKernel.second_fderiv_nonpos_at_localMax line 1741
182. lemma OAI.EllipticKernel.trace_mul_nonneg line 1768
183. lemma OAI.EllipticKernel.negative_potentialMatrix_posSemidef_at_localMax line 1780
184. lemma OAI.EllipticKernel.trace_potentialMatrix_nonpos_at_localMax line 1804
185. abbrev OAI.EllipticKernel.Bilin line 1822
186. abbrev OAI.EllipticKernel.SecondOrder line 1824
187. def OAI.EllipticKernel.realInner line 1830
188. lemma OAI.EllipticKernel.realInner_apply line 1832
189. def OAI.EllipticKernel.rankOne line 1835
190. def OAI.EllipticKernel.barrier line 1836
191. lemma OAI.EllipticKernel.barrier_smooth line 1838
192. lemma OAI.EllipticKernel.barrier_hasFDerivAt line 1841
193. lemma OAI.EllipticKernel.barrier_fderiv line 1852
194. lemma OAI.EllipticKernel.barrier_hessian line 1858
195. lemma OAI.EllipticKernel.continuous_rankOne line 1881
196. lemma OAI.EllipticKernel.exists_positive_barrier line 1888
197. lemma OAI.EllipticKernel.hessian_add line 1924
198. lemma OAI.EllipticKernel.hessian_add_smul_sub_const line 1941
199. lemma OAI.EllipticKernel.annulus_le_of_no_localMax line 1964
200. lemma OAI.EllipticKernel.tangent_ball line 2002
201. lemma OAI.EllipticKernel.no_tangent_max line 2052
202. theorem OAI.EllipticKernel.harmonic_eventually_eq_of_max line 2158
203. abbrev OAI.EllipticKernel.EC line 2186
204. def OAI.EllipticKernel.coordinateEquiv line 2193
205. lemma OAI.EllipticKernel.coordinateEquiv_apply line 2196
206. lemma OAI.EllipticKernel.coordinateEquiv_symm_apply line 2197
207. def OAI.EllipticKernel.pullBilin line 2200
208. lemma OAI.EllipticKernel.pullBilin_apply line 2204
209. lemma OAI.EllipticKernel.pullBilin_add line 2207
210. lemma OAI.EllipticKernel.pullBilin_smul line 2211
211. lemma OAI.EllipticKernel.hermitianPartMatrix_add line 2215
212. lemma OAI.EllipticKernel.hermitianPartMatrix_smul line 2223
213. def OAI.EllipticKernel.traceBilinLinear line 2230
214. def OAI.EllipticKernel.traceBilin line 2235
215. lemma OAI.EllipticKernel.traceBilin_apply line 2238
216. lemma OAI.EllipticKernel.traceBilin_continuousOn line 2241
217. lemma OAI.EllipticKernel.pullBilin_hessian line 2259
218. lemma OAI.EllipticKernel.traceBilin_localMax line 2270
219. lemma OAI.EllipticKernel.realInner_coordinate_single line 2287
220. lemma OAI.EllipticKernel.pull_rankOne line 2292
221. lemma OAI.EllipticKernel.traceBilin_symbol line 2302
222. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.continuous line 2319
223. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.euclidean_smooth line 2329
224. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.traceBilin_localExpression line 2334
225. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.harmonic_eventually_constant line 2350
226. theorem OAI.Anticanonical.SourceSmooth.linearizedMongeAmpere_kernel line 2386
227. def OAI.Anticanonical.SourceSmooth.SmoothRealFunction.normalizeAt line 2412
228. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.normalizeAt_value line 2416
229. lemma OAI.Anticanonical.SourceSmooth.SmoothRealFunction.hessian_normalizeAt line 2419
230. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.linearizedMongeAmpere_realSMul line 2431
231. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.linearizedMongeAmpere_normalizeAt line 2437
232. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.linearized_nonpos_at_globalMax line 2444
233. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.no_positive_constant_rhs line 2460
234. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.constant_rhs_eq_zero line 2472
235. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.normalized_augmented_kernel line 2487
236. def OAI.Anticanonical.SourceSmooth.HasNormalizedPoissonSolution line 2505