OAI/Geometry/EinsteinFour/HodgeTheory11.lean

GitHub source file

249 declarations, 0 contain sorry, 0 declared as axioms

The finite alternating Gram polynomial for degrees zero, one and two.

  1. abbrev OAI.PositiveEinsteinFour.Geometry.HeatEulerFiber line 23
  2. def OAI.PositiveEinsteinFour.Geometry.heatEulerUnit line 25
  3. def OAI.PositiveEinsteinFour.Geometry.heatEulerTrace line 27
  4. def OAI.PositiveEinsteinFour.Geometry.heatEulerGram line 29
  5. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerGram_add_left line 32
  6. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerGram_add_right line 38
  7. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerGram_smul_left line 43
  8. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerGram_smul_right line 51
  9. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerGram_comm line 59
  10. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerGram_unit_left line 67
  11. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerGram_unit_self line 71
  12. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerTrace_unit line 74
  13. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerGram_polynomial line 77
  14. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerGram_scalar_potential line 93
  15. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.eigen_evolution line 128
  16. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedResidual line 151
  17. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalized_eigen_evolution line 155
  18. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneResidual_as_amplitude line 187
  19. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneResidual_norm_le line 208
  20. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalOneResidualData line 221
  21. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residual line 298
  22. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalizedResidual line 301
  23. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.eigen_evolution line 307
  24. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalized_eigen_evolution line 327
  25. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalized_initial_eigen line 337
  26. theorem OAI.PositiveEinsteinFour.Geometry.heatScalarLift_tsupport line 365
  27. theorem OAI.PositiveEinsteinFour.Geometry.heatScalarOperator_tsupport line 372
  28. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.function_support line 392
  29. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.timeFunction_support line 399
  30. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residualAmplitude line 406
  31. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residualAmplitude_regular line 410
  32. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residualAmplitude_support line 418
  33. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residualFunction line 423
  34. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residualFunction_continuous line 426
  35. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residualFunction_support line 432
  36. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformColumn_growth line 461
  37. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformSignedIntegral_bound line 548
  38. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerAmplitude line 586
  39. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerAmplitude_zero line 591
  40. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerAmplitude_first_gram line 600
  41. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerSecondWeight line 623
  42. theorem OAI.PositiveEinsteinFour.Geometry.heatEuler_potential_density line 630
  43. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerSecondWeight_center line 644
  44. def OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.eulerAmplitude line 671
  45. def OAI.PositiveEinsteinFour.Geometry.heatFamilyEulerFirst line 675
  46. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyEulerFirst_regular line 679
  47. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.one_amplitude_family line 695
  48. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.scalar_amplitude_family line 703
  49. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.eulerFirst_zero_near line 711
  50. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformEulerFirst_quadratic line 726
  51. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.column_continuous line 769
  52. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.residual_continuous line 783
  53. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedColumn_continuous line 797
  54. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedResidual_continuous line 802
  55. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneColumn_continuous line 829
  56. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneResidual_continuous line 843
  57. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedColumn_continuous line 864
  58. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedResidual_continuous line 871
  59. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residualAmplitude_bound line 898
  60. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residualFunction_eq line 1016
  61. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residual_realization line 1047
  62. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerTrace_continuous line 1079
  63. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerGram_continuous line 1083
  64. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerAmplitude_continuous line 1094
  65. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerFirst line 1107
  66. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerTail line 1111
  67. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerPolynomial line 1123
  68. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerPolynomial_gram line 1128
  69. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerFirst_continuous line 1137
  70. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerFirst_compact line 1143
  71. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerFirst_zero_near line 1152
  72. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerTail_continuous line 1158
  73. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerTail_bound line 1183
  74. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerTail_zero line 1196
  75. def OAI.PositiveEinsteinFour.Geometry.heatResidualAtZero line 1219
  76. theorem OAI.PositiveEinsteinFour.Geometry.heatResidual_tendsto_zero line 1221
  77. theorem OAI.PositiveEinsteinFour.Geometry.heatResidualAtZero_continuous line 1235
  78. theorem OAI.PositiveEinsteinFour.Geometry.heatResidualAtZero_norm line 1243
  79. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalScalarLift_joint_continuous line 1268
  80. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.cutoff_joint_regular line 1302
  81. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residualAmplitude_joint_continuous line 1311
  82. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residual_continuous line 1337
  83. def OAI.PositiveEinsteinFour.Geometry.heatFamilyOnePolynomialColumn line 1370
  84. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOnePolynomialColumn_continuous line 1375
  85. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOnePolynomial_weight_bound line 1384
  86. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.onePolynomialColumn_family line 1419
  87. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformOnePolynomial_weight_bound line 1433
  88. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.one_transport line 1473
  89. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.one_amplitude_transport line 1490
  90. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.one_parametrix_residual line 1508
  91. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.euler_gaussian_limit line 1564
  92. def OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.eulerPolynomial line 1612
  93. def OAI.PositiveEinsteinFour.Geometry.heatFamilyEulerTail line 1617
  94. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.eulerAmplitude_continuous line 1629
  95. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyEulerTail_continuous line 1637
  96. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyEulerTail_bound line 1659
  97. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyEulerPolynomial_gram line 1674
  98. theorem OAI.PositiveEinsteinFour.Geometry.heat_norm_square_error_bound line 1702
  99. theorem OAI.PositiveEinsteinFour.Geometry.heat_norm_square_error_tendsto line 1720
  100. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedResidualZero line 1761
  101. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedResidual_bound line 1765
  102. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedResidualZero_continuous line 1774
  103. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedResidualZero_eq line 1782
  104. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedResidualZero_bound line 1789
  105. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedResidualZero line 1818
  106. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedResidual_bound line 1822
  107. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedResidualZero_continuous line 1831
  108. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedResidualZero_eq line 1839
  109. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedResidualZero_bound line 1846
  110. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.residual_norm_le line 1879
  111. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatScalarGlobalResidual line 1895
  112. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalizedResidualZero line 1911
  113. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalizedResidual_bound line 1914
  114. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalizedResidualZero_continuous line 1922
  115. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalizedResidualZero_eq line 1932
  116. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalizedResidualZero_bound line 1937
  117. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformOneColumn_growth line 1965
  118. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformOneCutoffResidual line 2052
  119. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.one_green_regular line 2149
  120. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.one_connection_operator line 2163
  121. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.actual_one_operator line 2178
  122. structure OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData line 2204
  123. def OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData.bundle line 2213
  124. def OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData.scalar line 2216
  125. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatEulerCommonChart line 2227
  126. theorem OAI.PositiveEinsteinFour.Geometry.heat_inner_error_bound line 2351
  127. theorem OAI.PositiveEinsteinFour.Geometry.heat_inner_error_tendsto line 2372
  128. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalized_eigen_integral line 2415
  129. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.one_normalized_eigen_integral line 2458
  130. theorem OAI.PositiveEinsteinFour.Geometry.scalar_eq_of_eigen_pairing line 2505
  131. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalized_eigen_integral line 2515
  132. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.spectral_comparison line 2533
  133. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.spectral_error_bound line 2552
  134. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatScalarSpectralComparison line 2565
  135. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformEulerIntegral_bound line 2593
  136. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.one_compact_green line 2631
  137. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_eq_of_eigen_pairing line 2723
  138. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.one_spectral_comparison line 2735
  139. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.one_spectral_error_bound line 2757
  140. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalOneSpectralComparison line 2773
  141. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.spectral_comparison line 2809
  142. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.spectral_error_bound line 2829
  143. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalSpectralComparison line 2843
  144. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.column_square_error_tendsto line 2879
  145. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.trace_gaussian_error_tendsto line 2893
  146. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatScalarTraceApproximation line 2910
  147. def OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.scalarData line 2938
  148. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.scalarData_actual line 2954
  149. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.one_compact_operator_pairing line 2971
  150. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.parametrixData_one_pairing line 2995
  151. theorem OAI.PositiveEinsteinFour.Geometry.heat_inner_error_uniform line 3030
  152. theorem OAI.PositiveEinsteinFour.Geometry.heat_signed_gram_error_uniform line 3045
  153. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatActualUniformSpectral line 3088
  154. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneColumn_square_error_tendsto line 3143
  155. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneTrace_error_tendsto line 3160
  156. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.column_square_error_tendsto line 3204
  157. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.trace_error_tendsto line 3220
  158. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.polynomial_weight_zero line 3262
  159. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalizedColumn_scaled_limit line 3273
  160. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeat_leading_pointwise_limit line 3301
  161. theorem OAI.PositiveEinsteinFour.Geometry.heat_norm_square_error_uniform line 3332
  162. theorem OAI.PositiveEinsteinFour.Geometry.heat_sum_norm_square_error_uniform line 3339
  163. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformOneSpectral line 3369
  164. def OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarPolynomial line 3416
  165. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarPolynomial_continuous line 3420
  166. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarPolynomial_weight_bound line 3426
  167. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.scalarPolynomial_family line 3451
  168. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformScalarPolynomial_weight_bound line 3464
  169. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.scalar_amplitude_transport line 3506
  170. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.scalar_parametrix_residual line 3522
  171. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformTwoSpectral line 3562
  172. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneColumn_norm_sq_integral line 3618
  173. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedColumn_norm_sq_integral line 3629
  174. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedColumn_gaussian_integral line 3638
  175. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneTrace_gaussian_error_tendsto line 3652
  176. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.column_norm_sq_integral line 3689
  177. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedColumn_norm_sq_integral line 3700
  178. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedColumn_gaussian_integral line 3709
  179. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.trace_gaussian_error_tendsto line 3721
  180. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformScalar_square_integral_bound line 3750
  181. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformScalarColumn_growth line 3784
  182. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformScalarNormalizedColumn_growth line 3806
  183. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformScalarCutoffResidual line 3834
  184. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedGram_columns line 3959
  185. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.column_inner_integral line 3971
  186. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedColumn_inner_integral line 3985
  187. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedColumn_gaussian_inner line 3996
  188. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalPolynomialColumn_zero line 4011
  189. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.polynomial_pair_integrable line 4020
  190. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.polynomial_weight_zero line 4063
  191. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedColumn_scaled_limit line 4078
  192. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.trace_scaled_limit line 4104
  193. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformScalarSpectral line 4147
  194. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalPolynomialColumn_matrix line 4191
  195. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalPolynomialColumn_signed line 4199
  196. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.signedColumn_integral line 4215
  197. theorem OAI.PositiveEinsteinFour.Geometry.heatEulerGram_columns line 4270
  198. theorem OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData.polynomial_scalar line 4284
  199. theorem OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData.polynomial_one line 4292
  200. theorem OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData.polynomial_two line 4305
  201. theorem OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData.polynomial_euler line 4313
  202. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealSignedTrace line 4344
  203. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealSignedTrace_columns line 4349
  204. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.column_inner_error_tendsto line 4360
  205. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.signed_trace_error_tendsto line 4381
  206. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerPolynomial_continuous line 4418
  207. theorem OAI.PositiveEinsteinFour.Geometry.heatEuler_cutoff_integrable line 4425
  208. theorem OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData.scalar_polynomial_integrable line 4438
  209. theorem OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData.one_polynomial_integrable line 4449
  210. theorem OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData.two_polynomial_integrable line 4467
  211. theorem OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData.euler_integral line 4474
  212. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.signed_trace_limit line 4534
  213. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.signed_trace_limit_unscaled line 4553
  214. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_signature_pointwise_limit line 4566
  215. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatSignedUniformLocal line 4596
  216. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.eulerPolynomial_scalar line 4653
  217. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.eulerPolynomial_one line 4675
  218. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.eulerPolynomial_two line 4683
  219. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.eulerPolynomial_gram line 4691
  220. def OAI.PositiveEinsteinFour.Geometry.hodgeHeatRealDensity line 4721
  221. theorem OAI.PositiveEinsteinFour.Geometry.hodgeHeatRealDensity_pos line 4727
  222. theorem OAI.PositiveEinsteinFour.Geometry.HeatEulerChartData.euler_trace_limit line 4736
  223. theorem OAI.PositiveEinsteinFour.Geometry.hodgeHeat_euler_pointwise_limit line 4771
  224. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatSignedUniformBase line 4805
  225. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatSignedUniformGlobal line 4821
  226. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.scalar_polynomial_integrable line 4852
  227. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.one_polynomial_integrable line 4867
  228. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.euler_integral line 4890
  229. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealSignedTrace_pos line 4955
  230. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealSignedTrace_nonpos line 4962
  231. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealSignedTrace_measurable line 4967
  232. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_signature_integral_limit line 4981
  233. theorem OAI.PositiveEinsteinFour.Geometry.harmonicSignature_eq_normalized_curvature_integral line 5010
  234. def OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.eulerColumnTrace line 5044
  235. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.eulerColumnTrace_integral line 5050
  236. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember.eulerColumnTrace_family line 5066
  237. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformEulerColumnTrace_bound line 5088
  238. theorem OAI.PositiveEinsteinFour.Geometry.riemannianChartFactor_toReal_pos line 5124
  239. theorem OAI.PositiveEinsteinFour.Geometry.normalizedChartFactor_inv_toReal line 5132
  240. theorem OAI.PositiveEinsteinFour.Geometry.deRhamSignature_eq_curvature_integral line 5138
  241. theorem OAI.PositiveEinsteinFour.Geometry.deRhamSignature_curvature_counts line 5148
  242. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformEulerDensity_bound line 5174
  243. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatEulerUniformLocal line 5258
  244. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatEulerUniformBase line 5272
  245. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatEulerUniformGlobal line 5287
  246. theorem OAI.PositiveEinsteinFour.Geometry.hodgeHeat_euler_integral_limit line 5318
  247. theorem OAI.PositiveEinsteinFour.Geometry.hodgeComplexEuler_eq_normalized_curvature_integral line 5355
  248. theorem OAI.PositiveEinsteinFour.Geometry.hodgeComplexEuler_eq_curvature_integral line 5368
  249. theorem OAI.PositiveEinsteinFour.Geometry.hodgeComplexEuler_curvature_counts line 5377