OAI/Geometry/EinsteinFour/HodgeTheory09.lean

GitHub source file

237 declarations, 0 contain sorry, 0 declared as axioms

The connection correction of a locally Sobolev two-form has one lower order divergence. The witnesses are actual Euclidean L2 functions.

  1. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFluxCorrection_memSobolev_successor line 46
  2. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFluxCorrection_integer_derivatives line 61
  3. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_inner_H3 line 107
  4. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_actual_local_H3 line 148
  5. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_continuous_coefficients line 200
  6. theorem OAI.PositiveEinsteinFour.Geometry.twoFormInnerNabla_component_integer line 268
  7. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonicDivergenceSource_integer line 278
  8. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigen_forcing_integer line 347
  9. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenDivergenceSource_integer line 368
  10. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_principalWeakInteger line 441
  11. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_weightedWeakInteger line 493
  12. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPoisson_forcing_integer line 555
  13. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPoissonDivergenceSource_integer line 573
  14. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRegularSource_forcing_integer line 646
  15. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRegularSourceDivergenceSource_integer line 664
  16. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigen_principalWeakInteger line 737
  17. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigen_weightedWeakInteger line 789
  18. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_weighted_integer line 856
  19. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPoisson_principalWeakInteger line 911
  20. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPoisson_weightedWeakInteger line 963
  21. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRegularSource_principalWeakInteger line 1035
  22. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRegularSource_weightedWeakInteger line 1087
  23. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigen_weighted_integer line 1154
  24. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_improved_representative line 1194
  25. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPoisson_weighted_integer line 1295
  26. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRegularSource_weighted_integer line 1355
  27. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigen_improved_representative line 1395
  28. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_local_all_orders line 1481
  29. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPoisson_improved_representative line 1535
  30. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRegularSource_improved_representative line 1621
  31. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigen_local_all_orders line 1712
  32. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_smooth_coefficients line 1767
  33. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPoisson_local_all_orders line 1834
  34. def OAI.PositiveEinsteinFour.Geometry.TwoFormChartSobolev line 1888
  35. theorem OAI.PositiveEinsteinFour.Geometry.TwoFormChartSobolev.mono line 1895
  36. theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartSobolev_one line 1902
  37. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRegularSource_chart_gain line 1909
  38. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedSolution_rough line 1931
  39. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedSolution_chart_gain line 1942
  40. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigen_smooth_coefficients line 1999
  41. theorem OAI.PositiveEinsteinFour.Geometry.twoFormResolvent_iterate_chart_order line 2072
  42. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatLift_chart_order line 2091
  43. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPoisson_smooth_coefficients line 2129
  44. theorem OAI.PositiveEinsteinFour.Geometry.twoForm_smooth_local_representative line 2196
  45. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigen_local_smooth line 2293
  46. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_local_smooth line 2353
  47. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatChartL2 line 2422
  48. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatChartL2_regular line 2428
  49. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatChartContinuous line 2434
  50. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatChartContinuous_ae line 2438
  51. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatChartContinuous_bound line 2443
  52. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_smooth_coefficients line 2470
  53. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPoisson_local_smooth line 2536
  54. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigen_smooth_representative line 2596
  55. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_smooth_representative line 2667
  56. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_local_smooth line 2738
  57. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPoisson_smooth_representative line 2797
  58. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_smooth_H1 line 2868
  59. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicToWeak_surjective line 2882
  60. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicWeakEquiv line 2889
  61. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_smooth_representative line 2915
  62. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothHodgePoisson line 2986
  63. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedSolution_unique line 3034
  64. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedSolution_harmonic line 3044
  65. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_harmonic line 3053
  66. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedSolution_mem_harmonic line 3059
  67. def OAI.PositiveEinsteinFour.Geometry.twoFormWeakHarmonicToResolvent line 3070
  68. def OAI.PositiveEinsteinFour.Geometry.twoFormWeakHarmonicResolventEquiv line 3080
  69. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicResolventEquiv line 3094
  70. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_eq_of_pairings line 3120
  71. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_eq_zero_iff line 3128
  72. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothHodgePoisson_pointwise line 3149
  73. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeForm_hodge_left line 3184
  74. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedSolution_hodge line 3190
  75. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_hodge line 3206
  76. theorem OAI.PositiveEinsteinFour.Geometry.twoFormResolvent_eigenspace_hodge line 3213
  77. def OAI.PositiveEinsteinFour.Geometry.twoFormHarmonicWeight line 3243
  78. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonicWeight_bound line 3247
  79. def OAI.PositiveEinsteinFour.Geometry.twoFormL2HarmonicProjection line 3252
  80. theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2HarmonicProjection_coordinate line 3256
  81. theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2HarmonicProjection_fixed line 3262
  82. theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2HarmonicProjection_smooth line 3273
  83. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatWeight_tendsto line 3286
  84. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_tendsto_harmonic line 3305
  85. def OAI.PositiveEinsteinFour.Geometry.twoFormHodgeDomain line 3333
  86. def OAI.PositiveEinsteinFour.Geometry.twoFormHodgeDomainEquiv line 3336
  87. def OAI.PositiveEinsteinFour.Geometry.twoFormHodgeGenerator line 3341
  88. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeDomain_dense line 3345
  89. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeDomain_weak line 3361
  90. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeDomain_of_weak line 3377
  91. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_mem_hodgeDomain line 3388
  92. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeGenerator_nonneg line 3392
  93. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeGenerator_symmetric line 3399
  94. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_add line 3432
  95. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_smul line 3447
  96. def OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacianLinear line 3460
  97. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_ker line 3466
  98. theorem OAI.PositiveEinsteinFour.Geometry.twoForm_weakEigen_rough line 3492
  99. theorem OAI.PositiveEinsteinFour.Geometry.twoForm_weakEigen_smooth line 3503
  100. theorem OAI.PositiveEinsteinFour.Geometry.twoFormResolvent_eigenvector_smooth line 3527
  101. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_weak line 3557
  102. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_mem_hodgeDomain line 3591
  103. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeGenerator_smooth line 3598
  104. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicL2 line 3637
  105. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicL2ToHarmonic line 3643
  106. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicL2ToHarmonic_injective line 3650
  107. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicL2_finite line 3655
  108. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothHarmonic_projection line 3663
  109. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothHodge_decomposition line 3673
  110. abbrev OAI.PositiveEinsteinFour.Geometry.TwoFormEigenIndex line 3702
  111. def OAI.PositiveEinsteinFour.Geometry.twoFormEigenvector line 3705
  112. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenvector_orthonormal line 3708
  113. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenvector_span line 3713
  114. def OAI.PositiveEinsteinFour.Geometry.twoFormEigenbasis line 3735
  115. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenvector_hasEigenvector line 3740
  116. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenvector_smooth line 3750
  117. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodiffPairing_add_right line 3775
  118. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_add_right line 3780
  119. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_hodge_left line 3785
  120. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_codiff_self line 3796
  121. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_codiff_pairing line 3804
  122. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_dDelta_hodge line 3822
  123. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothHodge_exact_coexact line 3831
  124. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodge_resolvent_of_distribution line 3862
  125. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeDomain_of_distribution line 3904
  126. def OAI.PositiveEinsteinFour.Geometry.twoFormEigenSection line 3942
  127. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenSection_L2 line 3945
  128. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenSection_equation line 3950
  129. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenSection_integral_norm line 3956
  130. def OAI.PositiveEinsteinFour.Geometry.twoFormFiniteHeatKernel line 3965
  131. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFiniteHeatKernel_diagonal line 3972
  132. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFiniteHeatKernel_trace_integral line 3983
  133. def OAI.PositiveEinsteinFour.Geometry.twoFormEigenform line 4018
  134. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenform_L2 line 4021
  135. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenform_laplacian line 4025
  136. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedSolution_dense line 4030
  137. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedSolution_eigen_smooth line 4037
  138. theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1_eigenforms_total line 4052
  139. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatChartContinuous_smooth line 4101
  140. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatChartContinuous_support line 4135
  141. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatChart_square_summable line 4145
  142. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_eigenvalue line 4174
  143. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_eigenvector line 4198
  144. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_closed_codiff_hodge line 4223
  145. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneForm_coexact_orthogonal_closed line 4249
  146. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothHodge_closed_decomposition line 4257
  147. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatConvolution line 4302
  148. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatConvolution_integrable line 4305
  149. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatConvolution_norm_le line 4313
  150. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatConvolution_eigen line 4327
  151. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatSection line 4369
  152. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatSection_H1 line 4372
  153. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatSection_L2 line 4377
  154. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_eq_dDelta_of_closed line 4402
  155. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothCoexact_of_divergence_eq_zero line 4418
  156. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferentialField_eq_zero_iff line 4464
  157. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_closed_iff_codifferential_hodge line 4480
  158. abbrev OAI.PositiveEinsteinFour.Geometry.smoothClosedTwoForms line 4532
  159. def OAI.PositiveEinsteinFour.Geometry.smoothExactTwoForms line 4541
  160. abbrev OAI.PositiveEinsteinFour.Geometry.TwoFormDeRhamCohomology line 4545
  161. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicToClosed line 4548
  162. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicToDeRham line 4554
  163. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicToDeRham_injective line 4560
  164. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicToDeRham_surjective line 4575
  165. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicDeRhamEquiv line 4589
  166. theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamCohomology_finite line 4594
  167. theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamCohomology_finrank line 4600
  168. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_local_diagonal line 4635
  169. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicPositive_star line 4683
  170. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicNegative_star line 4688
  171. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicSumLinear line 4693
  172. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicSumLinear_injective line 4700
  173. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicSumEquiv line 4714
  174. theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamCohomology_hodge_dimension line 4722
  175. abbrev OAI.PositiveEinsteinFour.Geometry.smoothCoClosedOneForms line 4749
  176. def OAI.PositiveEinsteinFour.Geometry.smoothCoexactOneForms line 4755
  177. abbrev OAI.PositiveEinsteinFour.Geometry.HodgeDualOneCohomology line 4759
  178. theorem OAI.PositiveEinsteinFour.Geometry.smoothCoexactOneForms_eq_top line 4764
  179. theorem OAI.PositiveEinsteinFour.Geometry.hodgeDualOneCohomology_eq_zero line 4772
  180. theorem OAI.PositiveEinsteinFour.Geometry.hodgeDualOneCohomology_subsingleton line 4780
  181. theorem OAI.PositiveEinsteinFour.Geometry.hodgeDualOneCohomology_finrank line 4785
  182. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneForm_eq_of_pairings line 4811
  183. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormDivergence_differential line 4819
  184. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeLaplacian_differential line 4826
  185. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_of_closed line 4834
  186. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_exterior line 4845
  187. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeLaplacian_codifferential line 4857
  188. theorem OAI.PositiveEinsteinFour.Geometry.scalarEigen_differential_is_oneFormEigen line 4868
  189. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothOneForm_Hodge_decomposition line 4898
  190. def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDDeltaLinear line 4945
  191. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDDeltaLinear_apply line 4948
  192. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDDelta_add line 4951
  193. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDDelta_smul line 4955
  194. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDDelta_hodge_DDelta line 4961
  195. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_hodge line 4970
  196. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDDelta_laplacian line 4977
  197. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_DDelta line 4983
  198. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDDelta_eigen_square line 4989
  199. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_local_diagonal_bound line 5015
  200. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_diagonal_bound line 5050
  201. def OAI.PositiveEinsteinFour.Geometry.smoothScalarMean line 5088
  202. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarMean_const line 5100
  203. abbrev OAI.PositiveEinsteinFour.Geometry.DivergenceCokernel line 5104
  204. def OAI.PositiveEinsteinFour.Geometry.divergenceCokernelMean line 5107
  205. theorem OAI.PositiveEinsteinFour.Geometry.mem_divergence_range_iff_mean_zero line 5115
  206. theorem OAI.PositiveEinsteinFour.Geometry.divergenceCokernelMean_zero line 5133
  207. theorem OAI.PositiveEinsteinFour.Geometry.divergenceCokernelMean_bijective line 5141
  208. def OAI.PositiveEinsteinFour.Geometry.divergenceCokernelEquiv line 5152
  209. theorem OAI.PositiveEinsteinFour.Geometry.divergenceCokernel_finrank line 5157
  210. theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_negative_harmonic_zero line 5185
  211. theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_negative_harmonic_dimension_zero line 5206
  212. def OAI.PositiveEinsteinFour.Geometry.oneFormDerivedFamily line 5238
  213. theorem OAI.PositiveEinsteinFour.Geometry.oneFormDerivedFamily_total line 5244
  214. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothOneFormHodgePoisson line 5305
  215. theorem OAI.PositiveEinsteinFour.Geometry.existsUnique_smoothOneFormHodgePoisson line 5335
  216. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatSection_eigen_integral line 5362
  217. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_weight_square_summable line 5376
  218. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_weight_summable line 5396
  219. def OAI.PositiveEinsteinFour.Geometry.twoFormIntersection line 5429
  220. theorem OAI.PositiveEinsteinFour.Geometry.twoFormIntersection_comm line 5432
  221. theorem OAI.PositiveEinsteinFour.Geometry.twoFormIntersection_add_left line 5437
  222. theorem OAI.PositiveEinsteinFour.Geometry.twoFormIntersection_smul_left line 5442
  223. theorem OAI.PositiveEinsteinFour.Geometry.twoFormIntersection_add_right line 5446
  224. theorem OAI.PositiveEinsteinFour.Geometry.twoFormIntersection_smul_right line 5451
  225. theorem OAI.PositiveEinsteinFour.Geometry.twoFormIntersection_exact_closed line 5455
  226. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicIntersection line 5463
  227. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicIntersection_nondegenerate line 5472
  228. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicIntersection_positive line 5481
  229. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicIntersection_negative line 5487
  230. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicIntersection_orthogonal line 5497
  231. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_resolvent_eigen line 5532
  232. def OAI.PositiveEinsteinFour.Geometry.TwoFormSmoothEigenSpace line 5562
  233. def OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenL2 line 5565
  234. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenL2_injective line 5578
  235. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenL2_surjective line 5584
  236. def OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenEquiv line 5596
  237. instance OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenFinite line 5602