OAI/Geometry/EinsteinFour/HeatKernels10.lean

GitHub source file

763 declarations, 0 contain sorry, 0 declared as axioms

The integral intersection form descends to the actual de Rham quotient and is nondegenerate there.

  1. def OAI.PositiveEinsteinFour.Geometry.smoothClosedIntersection line 57
  2. theorem OAI.PositiveEinsteinFour.Geometry.smoothClosedIntersection_exact_right line 66
  3. theorem OAI.PositiveEinsteinFour.Geometry.smoothClosedIntersection_exact_left line 75
  4. theorem OAI.PositiveEinsteinFour.Geometry.twoFormIntersection_sub_left line 81
  5. def OAI.PositiveEinsteinFour.Geometry.deRhamIntersection line 86
  6. theorem OAI.PositiveEinsteinFour.Geometry.harmonicRepresentative_intersection line 92
  7. theorem OAI.PositiveEinsteinFour.Geometry.deRhamIntersection_representatives line 108
  8. theorem OAI.PositiveEinsteinFour.Geometry.deRhamIntersection_comm line 121
  9. theorem OAI.PositiveEinsteinFour.Geometry.deRhamIntersection_nondegenerate line 126
  10. def OAI.PositiveEinsteinFour.Geometry.harmonicIntersectionQuadratic line 163
  11. theorem OAI.PositiveEinsteinFour.Geometry.harmonicIntersection_positive_definite line 166
  12. theorem OAI.PositiveEinsteinFour.Geometry.harmonicIntersection_negative_definite line 177
  13. theorem OAI.PositiveEinsteinFour.Geometry.harmonicIntersection_sigPos line 188
  14. theorem OAI.PositiveEinsteinFour.Geometry.harmonicIntersection_sigNeg line 204
  15. def OAI.PositiveEinsteinFour.Geometry.smoothOneFormWrap line 243
  16. def OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Linear line 248
  17. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Linear_injective line 251
  18. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Linear_inner line 255
  19. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Pairing_smul_right line 259
  20. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_exact_coexact_orthogonal line 264
  21. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneForm_eigen_orthogonal line 274
  22. def OAI.PositiveEinsteinFour.Geometry.oneFormCodiffEigenMap line 285
  23. def OAI.PositiveEinsteinFour.Geometry.OneFormCoexactSpectralSpace line 290
  24. instance OAI.PositiveEinsteinFour.Geometry.oneFormCoexactSpectralFinite line 294
  25. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactSpectral_representation line 300
  26. theorem OAI.PositiveEinsteinFour.Geometry.smoothCodiff_eigen line 308
  27. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactSpectral_orthogonal line 315
  28. def OAI.PositiveEinsteinFour.Geometry.smoothScalarPositiveLaplacian line 349
  29. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothPositivePoisson line 356
  30. def OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenDDelta line 394
  31. def OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenHodge line 406
  32. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenDDelta_square line 418
  33. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenDDelta_hodge_zero line 428
  34. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenHodge_anticommutator line 437
  35. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenHodge_trace_zero line 451
  36. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatSection_pointwise_square_summable line 483
  37. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernelTerm line 490
  38. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernelTerm_norm_summable line 496
  39. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernelTerm_summable line 508
  40. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel line 513
  41. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_hasSum line 517
  42. def OAI.PositiveEinsteinFour.Geometry.deRhamIntersectionQuadratic line 548
  43. def OAI.PositiveEinsteinFour.Geometry.harmonicDeRhamIntersectionIsometry line 552
  44. theorem OAI.PositiveEinsteinFour.Geometry.deRhamIntersection_sigPos line 563
  45. theorem OAI.PositiveEinsteinFour.Geometry.deRhamIntersection_sigNeg line 570
  46. def OAI.PositiveEinsteinFour.Geometry.deRhamSignature line 577
  47. theorem OAI.PositiveEinsteinFour.Geometry.deRhamSignature_hodge line 581
  48. theorem OAI.PositiveEinsteinFour.Geometry.smoothCodifferential_DDelta_eigen line 608
  49. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenCodiff_DDelta line 621
  50. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenCodiff_hodge_DDelta line 633
  51. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenHodge_square line 645
  52. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigen_DDelta_hodge_split line 653
  53. abbrev OAI.PositiveEinsteinFour.Geometry.OneFormCoexactEigenIndex line 685
  54. def OAI.PositiveEinsteinFour.Geometry.oneFormCoexactEigenvector line 689
  55. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactEigenvector_orthonormal line 692
  56. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexact_mem_span line 702
  57. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactEigenvector_smooth line 715
  58. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactEigenvector_rate_pos line 726
  59. theorem OAI.PositiveEinsteinFour.Geometry.scalarEigen_differential_inner line 767
  60. theorem OAI.PositiveEinsteinFour.Geometry.scalarEigen_differential_zero line 789
  61. abbrev OAI.PositiveEinsteinFour.Geometry.OneFormExactEigenIndex line 796
  62. def OAI.PositiveEinsteinFour.Geometry.oneFormExactEigenvector line 798
  63. theorem OAI.PositiveEinsteinFour.Geometry.oneFormExactEigenvector_orthonormal line 803
  64. def OAI.PositiveEinsteinFour.Geometry.smoothOneFormEuclideanValue line 844
  65. def OAI.PositiveEinsteinFour.Geometry.smoothOneFormFrameLinear line 849
  66. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormFrameLinear_norm line 867
  67. def OAI.PositiveEinsteinFour.Geometry.smoothOneFormFrameL2 line 884
  68. def OAI.PositiveEinsteinFour.Geometry.oneFormFrameL2 line 887
  69. theorem OAI.PositiveEinsteinFour.Geometry.oneFormFrameL2_smooth line 890
  70. theorem OAI.PositiveEinsteinFour.Geometry.oneFormFrameL2_norm line 895
  71. theorem OAI.PositiveEinsteinFour.Geometry.oneFormFrameL2_injective line 905
  72. def OAI.PositiveEinsteinFour.Geometry.twoFormFiberTrace line 928
  73. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFiberTrace_apply line 931
  74. instance OAI.PositiveEinsteinFour.Geometry.twoFormEigenIndexCountable line 938
  75. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_diagonal_trace line 947
  76. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatWeight_half_sq line 956
  77. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_trace_integral line 963
  78. def OAI.PositiveEinsteinFour.Geometry.twoFormEigenspaceHodge line 1006
  79. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSmoothEigenEquiv_hodge line 1012
  80. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenspaceHodge_conj line 1019
  81. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenspaceHodge_trace_zero line 1030
  82. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenspaceHodge_trace_basis line 1038
  83. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicHodge_trace line 1070
  84. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicResolventEquiv_val line 1096
  85. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicResolventEquiv_hodge line 1103
  86. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonicEigenspace_trace line 1114
  87. def OAI.PositiveEinsteinFour.Geometry.hodgeComplexEuler line 1159
  88. theorem OAI.PositiveEinsteinFour.Geometry.hodgeComplexEuler_hodge line 1166
  89. def OAI.PositiveEinsteinFour.Geometry.oneFormCoexactEigensection line 1199
  90. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactEigensection_L2 line 1203
  91. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactEigensection_eigen line 1208
  92. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactEigensection_divergence line 1213
  93. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactEigensection_codiff_exterior line 1217
  94. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexact_exterior_inner line 1227
  95. def OAI.PositiveEinsteinFour.Geometry.oneFormCoexactLift line 1238
  96. def OAI.PositiveEinsteinFour.Geometry.oneFormCoexactLiftL2 line 1242
  97. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactLift_orthonormal line 1245
  98. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactLift_codifferential line 1268
  99. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactLift_eigen line 1282
  100. theorem OAI.PositiveEinsteinFour.Geometry.twoForm_nonzero_coexact_multiplicity line 1312
  101. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexact_harmonic_eq_bot line 1354
  102. def OAI.PositiveEinsteinFour.Geometry.smoothOneFormContinuousLinear line 1393
  103. def OAI.PositiveEinsteinFour.Geometry.oneFormContinuousSubspace line 1402
  104. abbrev OAI.PositiveEinsteinFour.Geometry.OneFormC0 line 1405
  105. instance OAI.PositiveEinsteinFour.Geometry.oneFormC0_complete line 1407
  106. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormEuclideanValue_norm_base line 1411
  107. theorem OAI.PositiveEinsteinFour.Geometry.oneFormC0_norm_base line 1421
  108. def OAI.PositiveEinsteinFour.Geometry.oneFormC0BaseNorm line 1429
  109. theorem OAI.PositiveEinsteinFour.Geometry.oneFormC0BaseNorm_frame line 1432
  110. theorem OAI.PositiveEinsteinFour.Geometry.oneFormC0BaseNorm_continuous line 1437
  111. def OAI.PositiveEinsteinFour.Geometry.oneFormC0ToFrameLp line 1445
  112. theorem OAI.PositiveEinsteinFour.Geometry.oneFormC0ToFrameLp_norm_sq line 1448
  113. theorem OAI.PositiveEinsteinFour.Geometry.oneFormC0ToFrameLp_injective line 1465
  114. abbrev OAI.PositiveEinsteinFour.Geometry.OneFormEigenIndex line 1510
  115. def OAI.PositiveEinsteinFour.Geometry.oneFormEigenvector line 1512
  116. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_exact_coexact_eigen_orthogonal line 1516
  117. theorem OAI.PositiveEinsteinFour.Geometry.oneFormEigenvector_orthonormal line 1526
  118. theorem OAI.PositiveEinsteinFour.Geometry.oneFormEigenvector_total line 1549
  119. def OAI.PositiveEinsteinFour.Geometry.oneFormEigenbasis line 1587
  120. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatSection_eigen line 1611
  121. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernelTerm_eigen line 1627
  122. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_eigen_hasSum line 1646
  123. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatTwoForm_composition_bound line 1676
  124. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatTwoForm_composition_integrable line 1689
  125. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatTwoForm_composition_integral_bound line 1699
  126. def OAI.PositiveEinsteinFour.Geometry.hodgeComplexD2 line 1734
  127. theorem OAI.PositiveEinsteinFour.Geometry.hodgeComplexD2_kernel line 1737
  128. theorem OAI.PositiveEinsteinFour.Geometry.hodgeComplexD2_range line 1742
  129. theorem OAI.PositiveEinsteinFour.Geometry.hodgeComplex_D1_D0 line 1758
  130. theorem OAI.PositiveEinsteinFour.Geometry.hodgeComplex_D2_D1 line 1763
  131. theorem OAI.PositiveEinsteinFour.Geometry.hodgeComplex_D3_D2 line 1769
  132. theorem OAI.PositiveEinsteinFour.Geometry.oneFormFrameL2_inner line 1793
  133. def OAI.PositiveEinsteinFour.Geometry.oneFormFromFrameL2 line 1799
  134. theorem OAI.PositiveEinsteinFour.Geometry.oneFormFromFrameL2_pairing line 1802
  135. theorem OAI.PositiveEinsteinFour.Geometry.oneFormFromFrameL2_left_inverse line 1807
  136. def OAI.PositiveEinsteinFour.Geometry.oneFormFromContinuous line 1813
  137. theorem OAI.PositiveEinsteinFour.Geometry.oneFormFromContinuous_pairing line 1816
  138. theorem OAI.PositiveEinsteinFour.Geometry.oneFormFromContinuous_smooth line 1830
  139. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatRate line 1860
  140. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatRate_pos line 1865
  141. theorem OAI.PositiveEinsteinFour.Geometry.oneFormEigenvector_smooth line 1871
  142. def OAI.PositiveEinsteinFour.Geometry.modeSynthesis line 1904
  143. theorem OAI.PositiveEinsteinFour.Geometry.modeSynthesis_single line 1908
  144. theorem OAI.PositiveEinsteinFour.Geometry.modeAnalysis_coordinate line 1915
  145. def OAI.PositiveEinsteinFour.Geometry.oneFormCoexactSynthesis line 1932
  146. def OAI.PositiveEinsteinFour.Geometry.oneFormLiftSynthesis line 1935
  147. def OAI.PositiveEinsteinFour.Geometry.oneFormCoexactSpectralLift line 1938
  148. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactSpectralLift_eigen line 1942
  149. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactSpectralLift_exact line 1961
  150. def OAI.PositiveEinsteinFour.Geometry.oneFormExactSynthesis line 1977
  151. def OAI.PositiveEinsteinFour.Geometry.scalarPositiveSynthesis line 1980
  152. def OAI.PositiveEinsteinFour.Geometry.oneFormExactSpectralLift line 1984
  153. theorem OAI.PositiveEinsteinFour.Geometry.oneFormExactSpectralLift_eigen line 1988
  154. theorem OAI.PositiveEinsteinFour.Geometry.oneFormExactSpectralLift_coexact line 2004
  155. def OAI.PositiveEinsteinFour.Geometry.oneFormSpectralEquiv line 2042
  156. def OAI.PositiveEinsteinFour.Geometry.oneFormSpectralMultiplier line 2045
  157. theorem OAI.PositiveEinsteinFour.Geometry.oneFormSpectralMultiplier_coordinate line 2061
  158. theorem OAI.PositiveEinsteinFour.Geometry.oneFormSpectralMultiplier_norm line 2071
  159. theorem OAI.PositiveEinsteinFour.Geometry.oneFormSpectralMultiplier_inner line 2090
  160. theorem OAI.PositiveEinsteinFour.Geometry.oneFormSpectralMultiplier_selfAdjoint line 2101
  161. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatLift_smooth line 2140
  162. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_coexactLift line 2147
  163. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatLift_coexactLift line 2157
  164. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenbasis_apply line 2187
  165. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_pairing_hasSum line 2192
  166. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_pairing_tsum line 2209
  167. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_diagonal_power line 2235
  168. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_diagonal_remainder_tendsto line 2242
  169. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatTimePolynomial_bound line 2279
  170. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatTimePolynomial_integrable line 2296
  171. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCoordinates_continuousOn line 2330
  172. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitude line 2341
  173. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitudeL2 line 2355
  174. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitudeL2_pairing line 2362
  175. def OAI.PositiveEinsteinFour.Geometry.heatOneChart line 2387
  176. theorem OAI.PositiveEinsteinFour.Geometry.heatOneChart_smooth line 2396
  177. abbrev OAI.PositiveEinsteinFour.Geometry.HodgeEvenSections line 2443
  178. abbrev OAI.PositiveEinsteinFour.Geometry.HodgeOddSections line 2446
  179. def OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracEven line 2449
  180. def OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracOdd line 2459
  181. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracEven_apply line 2467
  182. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracOdd_apply line 2473
  183. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDirac_square_even line 2481
  184. theorem OAI.PositiveEinsteinFour.Geometry.oneFormFromFrameL2_norm_le line 2522
  185. theorem OAI.PositiveEinsteinFour.Geometry.oneFormFromContinuous_norm_le line 2538
  186. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatRate_nonneg line 2573
  187. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatWeight line 2576
  188. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatWeight_bound line 2581
  189. def OAI.PositiveEinsteinFour.Geometry.oneFormHeat line 2587
  190. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_coordinate line 2591
  191. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_zero line 2597
  192. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_add line 2605
  193. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_contraction line 2617
  194. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_selfAdjoint line 2622
  195. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_nonneg line 2626
  196. theorem OAI.PositiveEinsteinFour.Geometry.oneFormSpectralMultiplier_sub_norm_sq line 2654
  197. theorem OAI.PositiveEinsteinFour.Geometry.oneFormSpectralMultiplier_tendsto line 2673
  198. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEigenSection_pairing_integral_norm_bound line 2737
  199. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatFrameCoefficient line 2785
  200. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatFrameCoefficient_eq line 2789
  201. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatFrameCoefficient_mem line 2800
  202. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatFrameColumn line 2813
  203. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatFrameColumn_eigen line 2818
  204. theorem OAI.PositiveEinsteinFour.Geometry.twoForm_eq_of_eigen_pairing line 2826
  205. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatVolterra_step_bound line 2853
  206. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCoordinates_add line 2905
  207. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneFrameLift_add line 2916
  208. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitudeL2_add line 2928
  209. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitudeL2_continuous_family line 2975
  210. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitude_norm_sq line 3019
  211. theorem OAI.PositiveEinsteinFour.Geometry.heat_oneTensor_inner line 3065
  212. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneValue line 3087
  213. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneLift_pairing line 3091
  214. def OAI.PositiveEinsteinFour.Geometry.heatNormalParametrix line 3145
  215. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalParametrix_residual line 3149
  216. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalParametrix_diagonal_residual_tendsto line 3169
  217. theorem OAI.PositiveEinsteinFour.Geometry.fourSpace_norm_le_sum line 3205
  218. theorem OAI.PositiveEinsteinFour.Geometry.heatOneChart_bound line 3219
  219. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Pairing_differential line 3290
  220. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Pairing_codifferential line 3298
  221. def OAI.PositiveEinsteinFour.Geometry.smoothHodgeEvenPairing line 3307
  222. def OAI.PositiveEinsteinFour.Geometry.smoothHodgeOddPairing line 3312
  223. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDirac_adjoint line 3315
  224. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracOdd_kernel line 3364
  225. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracEven_kernel line 3393
  226. def OAI.PositiveEinsteinFour.Geometry.smoothOneFormFiber line 3437
  227. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormFiber_add line 3441
  228. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormFiber_sub line 3448
  229. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormFiber_differential line 3454
  230. def OAI.PositiveEinsteinFour.Geometry.twoFormCodifferentialFiber line 3459
  231. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormFiber_codifferential line 3462
  232. def OAI.PositiveEinsteinFour.Geometry.hodgeEvenFrameValue line 3467
  233. def OAI.PositiveEinsteinFour.Geometry.hodgeOddFrameValue line 3470
  234. def OAI.PositiveEinsteinFour.Geometry.hodgeEvenProduct line 3473
  235. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracEven_frame line 3477
  236. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormHodge_product line 3489
  237. theorem OAI.PositiveEinsteinFour.Geometry.scalarDifferentialFiber_product line 3498
  238. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodifferentialFiber_product line 3507
  239. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracEven_principalSymbol line 3515
  240. def OAI.PositiveEinsteinFour.Geometry.signatureEvenGrading line 3565
  241. def OAI.PositiveEinsteinFour.Geometry.signatureOddGrading line 3573
  242. theorem OAI.PositiveEinsteinFour.Geometry.signatureEvenGrading_apply line 3576
  243. theorem OAI.PositiveEinsteinFour.Geometry.signatureOddGrading_apply line 3580
  244. theorem OAI.PositiveEinsteinFour.Geometry.signatureEvenGrading_involutive line 3583
  245. theorem OAI.PositiveEinsteinFour.Geometry.signatureOddGrading_involutive line 3589
  246. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracEven_signature line 3593
  247. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracOdd_signature line 3613
  248. abbrev OAI.PositiveEinsteinFour.Geometry.HodgeSections line 3632
  249. def OAI.PositiveEinsteinFour.Geometry.smoothHodgeDirac line 3634
  250. def OAI.PositiveEinsteinFour.Geometry.signatureGrading line 3638
  251. theorem OAI.PositiveEinsteinFour.Geometry.signatureGrading_involutive line 3642
  252. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDirac_signature line 3646
  253. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_eigenvector line 3674
  254. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_continuous line 3693
  255. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatWeight_tendsto_zero line 3707
  256. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_tendsto_zero line 3715
  257. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexact_finrank_le line 3752
  258. def OAI.PositiveEinsteinFour.Geometry.oneFormCoexactToTwoFormIndex line 3759
  259. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactToTwoFormIndex_injective line 3764
  260. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_weight_summable line 3775
  261. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatTrace line 3788
  262. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatTrace_nonneg line 3791
  263. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatFrameCoefficient_sq_summable line 3815
  264. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatFrameColumn_norm_sq line 3823
  265. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_trace_columns line 3834
  266. def OAI.PositiveEinsteinFour.Geometry.twoFormKernelPairingMap line 3868
  267. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernelPairingTerm line 3879
  268. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_pairing_hasSum line 3885
  269. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernelPairingTerm_integrable line 3905
  270. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernelPairingTerm_integral_norm line 3917
  271. def OAI.PositiveEinsteinFour.Geometry.fourHeatVolterraIterate line 3953
  272. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatVolterraIterate_bound line 3959
  273. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatVolterra_majorant_summable line 3981
  274. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatVolterraIterate_norm_summable line 3990
  275. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatVolterraIterate_summable line 3999
  276. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitudeL2_norm_le line 4025
  277. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitudeL2_pairing_base line 4073
  278. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_le_diagonal line 4131
  279. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalParametrix_residual_bound line 4143
  280. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalParametrix_residual_uniform_linear line 4182
  281. theorem OAI.PositiveEinsteinFour.Geometry.heatOneChart_sub line 4224
  282. theorem OAI.PositiveEinsteinFour.Geometry.heatOneChart_smooth_approx line 4248
  283. def OAI.PositiveEinsteinFour.Geometry.scalarHeatSpectralTrace line 4304
  284. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatSpectralTrace line 4306
  285. def OAI.PositiveEinsteinFour.Geometry.oneFormExactHeatTrace line 4309
  286. def OAI.PositiveEinsteinFour.Geometry.oneFormCoexactHeatTrace line 4312
  287. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatTrace_split line 4316
  288. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatTrace_grouped line 4323
  289. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactHeatTrace_grouped line 4333
  290. theorem OAI.PositiveEinsteinFour.Geometry.twoForm_heat_multiplicity_term line 4347
  291. abbrev OAI.PositiveEinsteinFour.Geometry.HodgeEvenKernel line 4381
  292. abbrev OAI.PositiveEinsteinFour.Geometry.HodgeOddKernel line 4382
  293. def OAI.PositiveEinsteinFour.Geometry.harmonicToEvenKernel line 4393
  294. theorem OAI.PositiveEinsteinFour.Geometry.harmonicToEvenKernel_injective line 4407
  295. theorem OAI.PositiveEinsteinFour.Geometry.hodgeOddKernel_subsingleton line 4418
  296. theorem OAI.PositiveEinsteinFour.Geometry.hodgeOddKernel_finrank line 4425
  297. theorem OAI.PositiveEinsteinFour.Geometry.harmonicToEvenKernel_surjective line 4432
  298. def OAI.PositiveEinsteinFour.Geometry.harmonicEvenKernelEquiv line 4440
  299. theorem OAI.PositiveEinsteinFour.Geometry.hodgeEvenKernel_finite line 4445
  300. theorem OAI.PositiveEinsteinFour.Geometry.hodgeEvenKernel_finrank line 4451
  301. def OAI.PositiveEinsteinFour.Geometry.hodgeDiracKernelDifference line 4459
  302. theorem OAI.PositiveEinsteinFour.Geometry.hodgeDiracKernelDifference_hodge line 4463
  303. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothEvenHodgePoisson line 4494
  304. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracOdd_injective line 4507
  305. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracEven_surjective line 4516
  306. def OAI.PositiveEinsteinFour.Geometry.smoothHodgePairing line 4558
  307. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeEvenPairing_comm line 4561
  308. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeOddPairing_comm line 4567
  309. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgePairing_comm line 4572
  310. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgePairing_definite line 4577
  311. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDirac_selfAdjoint line 4604
  312. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgePairing_zero_right line 4614
  313. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_joint_continuous line 4634
  314. theorem OAI.PositiveEinsteinFour.Geometry.finite_positive_lower_bound line 4683

    Distinct definitions of this name: OAI/Geometry/EinsteinFour/GeodesicGeometry04.lean:1864 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.finite_positive_lower_bound@path.

  315. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatRate_lower_bound line 4703
  316. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatRate_inv_sqrt_bound line 4725
  317. def OAI.PositiveEinsteinFour.Geometry.signaturePositiveSections line 4752
  318. def OAI.PositiveEinsteinFour.Geometry.signatureNegativeSections line 4755
  319. theorem OAI.PositiveEinsteinFour.Geometry.signaturePositive_star line 4764
  320. theorem OAI.PositiveEinsteinFour.Geometry.signatureNegative_star line 4768
  321. def OAI.PositiveEinsteinFour.Geometry.signatureOperator line 4772
  322. def OAI.PositiveEinsteinFour.Geometry.signatureOperatorOpposite line 4786
  323. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernelPairingTerm_integral_norm_summable line 4821
  324. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_pairing_integrable line 4844
  325. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernelPairingTerm_integral line 4859
  326. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_pairing_integral line 4883
  327. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealColumn line 4921
  328. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealColumn_pos line 4925
  329. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealTrace line 4931
  330. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealTrace_columns line 4936
  331. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalBundleParametrix_residual_bound line 4964
  332. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalBundleParametrix_residual_uniform_linear line 5020
  333. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitudeL2_pairing_normal line 5060
  334. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneParametrix_residual_bound line 5099
  335. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneParametrix_residual_uniform_linear line 5155
  336. theorem OAI.PositiveEinsteinFour.Geometry.heatOneChart_L2_realization line 5191
  337. theorem OAI.PositiveEinsteinFour.Geometry.heatOneChart_L2_norm line 5213
  338. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformCutoffResidual line 5252
  339. theorem OAI.PositiveEinsteinFour.Geometry.hodgeDiracEven_cokernel_subsingleton line 5354
  340. theorem OAI.PositiveEinsteinFour.Geometry.hodgeDiracEven_finite_kernel_cokernel line 5359
  341. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracEven_index line 5368
  342. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeDiracEven_index_eq_euler line 5379
  343. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothHodge_full_decomposition line 5404
  344. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatConvolution line 5467
  345. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatConvolution_integrable line 5470
  346. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatConvolution_norm_le line 5478
  347. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatConvolution_eigen line 5492
  348. def OAI.PositiveEinsteinFour.Geometry.oneFormInverseSquareRoot line 5537
  349. theorem OAI.PositiveEinsteinFour.Geometry.oneFormInverseSquareRoot_eigen line 5543
  350. def OAI.PositiveEinsteinFour.Geometry.oneFormScalarPotential line 5562
  351. def OAI.PositiveEinsteinFour.Geometry.oneFormTwoFormPotential line 5565
  352. theorem OAI.PositiveEinsteinFour.Geometry.oneFormScalarPotential_exact line 5568
  353. theorem OAI.PositiveEinsteinFour.Geometry.oneFormScalarPotential_coexact line 5577
  354. theorem OAI.PositiveEinsteinFour.Geometry.oneFormTwoFormPotential_coexact line 5585
  355. theorem OAI.PositiveEinsteinFour.Geometry.oneFormTwoFormPotential_exact line 5594
  356. abbrev OAI.PositiveEinsteinFour.Geometry.SignaturePositiveKernel line 5624
  357. abbrev OAI.PositiveEinsteinFour.Geometry.SignatureNegativeKernel line 5625
  358. theorem OAI.PositiveEinsteinFour.Geometry.signaturePositiveKernel_data line 5627
  359. theorem OAI.PositiveEinsteinFour.Geometry.signatureNegativeKernel_data line 5649
  360. def OAI.PositiveEinsteinFour.Geometry.signaturePlusMap line 5696
  361. def OAI.PositiveEinsteinFour.Geometry.signatureMinusMap line 5704
  362. theorem OAI.PositiveEinsteinFour.Geometry.signaturePlusMap_self line 5713
  363. theorem OAI.PositiveEinsteinFour.Geometry.signatureMinusMap_self line 5720
  364. theorem OAI.PositiveEinsteinFour.Geometry.signaturePlusMap_dirac line 5727
  365. theorem OAI.PositiveEinsteinFour.Geometry.signatureMinusMap_dirac line 5735
  366. theorem OAI.PositiveEinsteinFour.Geometry.tsum_eigenvalue_finrank line 5759
  367. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeat_zero_weight_summable line 5791
  368. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeat_zero_weight_sum line 5802
  369. def OAI.PositiveEinsteinFour.Geometry.twoFormFiberSignedTrace line 5829
  370. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFiberSignedTrace_rankOne line 5833
  371. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_signed_diagonal line 5848
  372. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_hodge_pairing_integral line 5858
  373. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatSection_signed_integral line 5871
  374. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_signed_integral line 5883
  375. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatActualUniformResidual line 5933
  376. def OAI.PositiveEinsteinFour.Geometry.heatCompactOneLift line 5981
  377. theorem OAI.PositiveEinsteinFour.Geometry.heatCompactOneLift_support line 5986
  378. theorem OAI.PositiveEinsteinFour.Geometry.heatCompactOneLift_tsupport line 5996
  379. theorem OAI.PositiveEinsteinFour.Geometry.heatCompactOneLift_continuous line 6003
  380. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffParametrix_bound_of_support line 6045
  381. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffParametrix_bound line 6118
  382. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffParametrix line 6156
  383. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneParametrix_space_regular line 6159
  384. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffColumn line 6167
  385. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffColumn_regular line 6171
  386. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffColumn_support line 6178
  387. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneTimeColumn line 6191
  388. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneTimeColumn_component line 6196
  389. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneTimeColumn_regular line 6203
  390. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneTimeColumn_support line 6218
  391. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneGlobalColumn line 6233
  392. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneGlobalTimeColumn line 6243
  393. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatReconstructed line 6279
  394. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatReconstructed_exact line 6283
  395. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatReconstructed_coexact line 6295
  396. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_reconstructed line 6315
  397. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatTrace_split line 6362
  398. def OAI.PositiveEinsteinFour.Geometry.signatureNegativeKernel_harmonic line 6419
  399. def OAI.PositiveEinsteinFour.Geometry.signatureNegativeCoordinates line 6427
  400. theorem OAI.PositiveEinsteinFour.Geometry.signatureNegativeCoordinates_injective line 6433
  401. theorem OAI.PositiveEinsteinFour.Geometry.signatureNegativeCoordinates_surjective line 6454
  402. def OAI.PositiveEinsteinFour.Geometry.signatureNegativeKernelEquiv line 6478
  403. theorem OAI.PositiveEinsteinFour.Geometry.signatureNegativeKernel_finite line 6483
  404. theorem OAI.PositiveEinsteinFour.Geometry.signatureNegativeKernel_finrank line 6488
  405. def OAI.PositiveEinsteinFour.Geometry.signaturePositiveKernel_harmonic line 6523
  406. def OAI.PositiveEinsteinFour.Geometry.signaturePositiveCoordinates line 6531
  407. theorem OAI.PositiveEinsteinFour.Geometry.signaturePositiveCoordinates_injective line 6537
  408. theorem OAI.PositiveEinsteinFour.Geometry.signaturePositiveCoordinates_surjective line 6558
  409. def OAI.PositiveEinsteinFour.Geometry.signaturePositiveKernelEquiv line 6584
  410. theorem OAI.PositiveEinsteinFour.Geometry.signaturePositiveKernel_finite line 6589
  411. theorem OAI.PositiveEinsteinFour.Geometry.signaturePositiveKernel_finrank line 6594
  412. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_signed_summable line 6621
  413. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_spectral_signed_trace line 6633
  414. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_signature_trace line 6680
  415. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodge_inner_coordinates line 6704
  416. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatFrameColumn_inner line 6720
  417. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatFrameCoefficient_product_summable line 6732
  418. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatKernel_signed_columns line 6741
  419. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_grouped_summable line 6795
  420. theorem OAI.PositiveEinsteinFour.Geometry.oneFormCoexactHeat_grouped_summable line 6804
  421. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatTrace_split line 6817
  422. def OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffColumn line 6864
  423. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffColumn_regular line 6868
  424. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffColumn_support line 6875
  425. def OAI.PositiveEinsteinFour.Geometry.heatNormalGlobalParametrixColumn line 6890
  426. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneChart_realization line 6921
  427. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneTensor_L2_realization line 6962
  428. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneParametrix_time_differentiable line 7016
  429. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffParametrix_residual_identity line 7023
  430. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneResidualColumn line 7069
  431. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneResidualColumn_component line 7073
  432. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneResidualColumn_regular line 7083
  433. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneResidualColumn_support line 7089
  434. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneResidualColumn_bound line 7095
  435. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffParametrix_pairing_deriv line 7130
  436. theorem OAI.PositiveEinsteinFour.Geometry.hodgeHeat_supertrace line 7183
  437. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeat_smooth_representative line 7219
  438. theorem OAI.PositiveEinsteinFour.Geometry.exists_signatureNegative_decomposition line 7266
  439. theorem OAI.PositiveEinsteinFour.Geometry.signatureNegative_exact_eq_zero line 7279
  440. abbrev OAI.PositiveEinsteinFour.Geometry.SignatureCokernel line 7294
  441. def OAI.PositiveEinsteinFour.Geometry.signatureNegativeToCokernel line 7297
  442. theorem OAI.PositiveEinsteinFour.Geometry.signatureNegativeToCokernel_injective line 7303
  443. theorem OAI.PositiveEinsteinFour.Geometry.signatureNegativeToCokernel_surjective line 7312
  444. def OAI.PositiveEinsteinFour.Geometry.signatureCokernelEquiv line 7325
  445. theorem OAI.PositiveEinsteinFour.Geometry.signatureCokernel_finite line 7331
  446. theorem OAI.PositiveEinsteinFour.Geometry.signatureCokernel_finrank line 7337
  447. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_series line 7362
  448. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatLiftSource_eigen line 7376
  449. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatDerivative line 7390
  450. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatDerivative_eigen line 7394
  451. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatDerivative_series line 7404
  452. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalGlobalParametrixColumn_initial line 7445
  453. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffParametrix_residual_zero line 7529
  454. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitude_L2_realization line 7575
  455. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitudeL2_norm_sq_integral line 7589
  456. def OAI.PositiveEinsteinFour.Geometry.heatNormalOperatorAmplitude line 7667
  457. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOperatorAmplitude_regular line 7672
  458. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOperatorAmplitude_support line 7685
  459. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffColumn_regular_four line 7702
  460. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffParametrix_pairing_deriv line 7735
  461. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatC0Value line 7788
  462. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatC0Value_L2 line 7792
  463. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatC0Linear line 7800
  464. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatC0_graph_closed line 7811
  465. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatC0_continuous line 7829
  466. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatToC0 line 7834
  467. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatToContinuous line 7838
  468. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatToContinuous_bound line 7841
  469. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatToContinuous_smooth line 7845
  470. theorem OAI.PositiveEinsteinFour.Geometry.signatureOperator_finite_kernel_cokernel line 7882
  471. theorem OAI.PositiveEinsteinFour.Geometry.signatureOperator_index line 7887
  472. theorem OAI.PositiveEinsteinFour.Geometry.signatureOperator_index_eq_signature line 7898
  473. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_rate_weight_summable line 7923
  474. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealTerm line 7949
  475. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealDerivativeTerm line 7954
  476. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealDerivativeTerm_bound line 7959
  477. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.potential_symmetric line 7997
  478. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.green_regular_near line 8016
  479. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.connection_operator_near line 8037
  480. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffParametrix_bound_of_support line 8071
  481. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffParametrix_bound line 8144
  482. def OAI.PositiveEinsteinFour.Geometry.heatNormalTimeColumn line 8187
  483. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalTimeColumn_component line 8192
  484. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalTimeColumn_regular line 8199
  485. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalTimeColumn_support line 8214
  486. def OAI.PositiveEinsteinFour.Geometry.heatNormalGlobalTimeColumn line 8229
  487. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.value_zero line 8260
  488. def OAI.PositiveEinsteinFour.Geometry.heatNormalizedParametrixColumn line 8270
  489. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalizedParametrixColumn_initial line 8278
  490. def OAI.PositiveEinsteinFour.Geometry.oneFormEigenSection line 8321
  491. theorem OAI.PositiveEinsteinFour.Geometry.oneFormEigenSection_L2 line 8325
  492. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatEvaluation line 8329
  493. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatFrameColumn line 8333
  494. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatFrameColumn_pairing line 8336
  495. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatFrameColumn_norm line 8341
  496. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatContinuous_eigen line 8350
  497. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatFrameColumn_eigen line 8360
  498. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealTerm_derivative line 8387
  499. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatRealTerm_hasSum line 8405
  500. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_hasDerivAt line 8411
  501. theorem OAI.PositiveEinsteinFour.Geometry.heatAmplitude_component_support line 8451
  502. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.compact_operator_eq line 8465
  503. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_joint_contDiffAt line 8507
  504. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial_joint_contDiff line 8518
  505. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffParametrix_joint_contDiffAt line 8531
  506. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalTimeColumn_joint_continuousOn line 8541
  507. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneGreen_regular_near line 8568
  508. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.connection_operator_near line 8580
  509. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.actual_one_operator_uniform_near line 8598
  510. theorem OAI.PositiveEinsteinFour.Geometry.heat_six_norm_le line 8632
  511. def OAI.PositiveEinsteinFour.Geometry.heatNormalResidualColumn line 8650
  512. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalResidualColumn_component line 8654
  513. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalResidualColumn_regular line 8664
  514. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalResidualColumn_support line 8670
  515. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalResidualColumn_bound line 8676
  516. theorem OAI.PositiveEinsteinFour.Geometry.heatConnectionZero_signed_trace line 8704
  517. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.connection_partial_signed_trace line 8731
  518. def OAI.PositiveEinsteinFour.Geometry.heatNormalConnectionQuadratic line 8742
  519. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.bundleZero_signed_near line 8747
  520. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.C_signed_near line 8762
  521. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.exponential_source line 8792
  522. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.frame_det line 8798
  523. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.green_regular line 8805
  524. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.connection_operator line 8836
  525. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.actual_bundle_operator line 8850
  526. instance OAI.PositiveEinsteinFour.Geometry.oneFormEigenIndex_countable line 8885
  527. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatWeight_half_sq line 8894
  528. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatDiagonal line 8900
  529. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatFrameColumn_norm_sq line 8903
  530. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatFrameCoefficient_sq_summable line 8915
  531. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatDiagonal_summable line 8927
  532. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatDiagonal_columns line 8944
  533. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatDiagonal_nonneg line 8958
  534. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatDiagonal_bound line 8963
  535. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatDerivative_generator line 8997
  536. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatDerivative_laplacian line 9013
  537. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_geometric_equation line 9027
  538. theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnectionMatrix_trace line 9051
  539. theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnectionMatrix_square_trace line 9056
  540. theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnectionMatrix_product_trace line 9064
  541. theorem OAI.PositiveEinsteinFour.Geometry.heatFour_skew_trace line 9082
  542. theorem OAI.PositiveEinsteinFour.Geometry.heatOneConnectionZero_trace line 9087
  543. theorem OAI.PositiveEinsteinFour.Geometry.heatTwoConnectionZero_trace line 9098
  544. theorem OAI.PositiveEinsteinFour.Geometry.heat_weighted_inner_sum line 9126
  545. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.compact_green_near line 9139
  546. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeL2_pairing_sum line 9237
  547. theorem OAI.PositiveEinsteinFour.Geometry.heatOneAmplitude_component_support line 9294
  548. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.compact_operator_eq line 9308
  549. theorem OAI.PositiveEinsteinFour.Geometry.heat_one_weighted_inner_sum line 9339
  550. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.compact_green_near line 9352
  551. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffParametrix_joint_contDiffAt line 9451
  552. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneTimeColumn_joint_continuousOn line 9461
  553. def OAI.PositiveEinsteinFour.Geometry.heatNormalPolynomialColumn line 9493
  554. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalPolynomialColumn_continuous line 9497
  555. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffColumn_gaussian line 9507
  556. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalPolynomialColumn_weight_bound line 9517
  557. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffColumn_joint_continuousOn line 9559
  558. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOperatorColumn_joint_continuousOn line 9568
  559. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalResidualColumn_joint_continuousOn line 9584
  560. theorem OAI.PositiveEinsteinFour.Geometry.heat_trace_product_expansion line 9608
  561. theorem OAI.PositiveEinsteinFour.Geometry.heat_trace_product_regular line 9614
  562. theorem OAI.PositiveEinsteinFour.Geometry.heat_trace_product_partial_zero line 9622
  563. theorem OAI.PositiveEinsteinFour.Geometry.heat_weighted_trace_second_zero line 9644
  564. theorem OAI.PositiveEinsteinFour.Geometry.heat_weighted_trace_partial_zero line 9658
  565. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.quadratic_zero line 9673
  566. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.quadratic_partial_zero line 9678
  567. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.quadratic_second line 9696
  568. theorem OAI.PositiveEinsteinFour.Geometry.oneFormEigenSection_norm_integral line 9747
  569. theorem OAI.PositiveEinsteinFour.Geometry.oneFormEigenSection_norm_nonneg line 9754
  570. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatDiagonal_integrable line 9760
  571. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatDiagonal_integral line 9781
  572. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatRealColumn line 9823
  573. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatRealColumn_pos line 9826
  574. def OAI.PositiveEinsteinFour.Geometry.oneFormHeatRealDiagonal line 9831
  575. theorem OAI.PositiveEinsteinFour.Geometry.oneFormHeatRealDiagonal_columns line 9834
  576. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_zero_solution line 9864
  577. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_evolution_unique line 9891
  578. theorem OAI.PositiveEinsteinFour.Geometry.heatFourTrace_partial line 9938
  579. theorem OAI.PositiveEinsteinFour.Geometry.heatSixTrace_partial line 9944
  580. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneConnection_partial_trace line 9954
  581. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.twoConnection_partial_trace line 9966
  582. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleOperator_leading line 9993
  583. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_leading_signed_source line 10008
  584. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.firstSource line 10043
  585. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.firstSource_regular line 10048
  586. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.B_signed_near line 10063
  587. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.firstSource_signed_near line 10073
  588. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.first_amplitude_signed_radial line 10083
  589. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffColumn_square_integral_bound line 10116
  590. def OAI.PositiveEinsteinFour.Geometry.heatNormalHodgeImage line 10170
  591. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.compact_hodge_domain_near line 10181
  592. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneAmplitudeL2_pairing_sum line 10230
  593. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneHodgeImage line 10297
  594. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.compact_operator_pairing_near line 10308
  595. def OAI.PositiveEinsteinFour.Geometry.heatNormalOnePolynomialColumn line 10355
  596. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOnePolynomialColumn_continuous line 10359
  597. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffColumn_gaussian line 10369
  598. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOnePolynomialColumn_weight_bound line 10379
  599. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffColumn_joint_continuousOn line 10421
  600. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneOperatorColumn_joint_continuousOn line 10430
  601. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneResidualColumn_joint_continuousOn line 10446
  602. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalGlobalParametrixColumn_weak_deriv line 10476
  603. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.compact_green line 10548
  604. def OAI.PositiveEinsteinFour.Geometry.heatFamilyPolynomialColumn line 10632
  605. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyPolynomialColumn_continuous line 10637
  606. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyPolynomial_weight_bound line 10646
  607. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.polynomialColumn_family line 10681
  608. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformPolynomial_weight_bound line 10695
  609. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatDiagonal_integrable line 10745
  610. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatDiagonal_integrable line 10753
  611. def OAI.PositiveEinsteinFour.Geometry.hodgeHeatDensity line 10771
  612. theorem OAI.PositiveEinsteinFour.Geometry.hodgeHeatDensity_integrable line 10775
  613. theorem OAI.PositiveEinsteinFour.Geometry.hodgeHeatDensity_integral line 10781
  614. theorem OAI.PositiveEinsteinFour.Geometry.heat_partial_second_germ line 10815
  615. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage_second_of_vanishing_jet line 10822
  616. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.quadratic_second_curvature line 10839
  617. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.first_amplitude_signed_second line 10860
  618. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.first_amplitude_signed_partial line 10897
  619. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.bundleOne_trace_relation_near line 10938
  620. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffColumn_square_integral_bound line 10997
  621. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneGlobalColumn_weak_deriv line 11051
  622. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.parametrix_domain_near line 11127
  623. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalizedParametrixColumn_domain line 11153
  624. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.compact_hodge_domain line 11193
  625. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneOperator_leading line 11229
  626. theorem OAI.PositiveEinsteinFour.Geometry.heatOneLeadingSource_trace line 11244
  627. theorem OAI.PositiveEinsteinFour.Geometry.heatTwoLeadingSource_trace line 11271
  628. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.oneCompanion line 11303
  629. def OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.firstSource line 11307
  630. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.firstSource_regular line 11311
  631. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.B_trace_near line 11326
  632. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.B_trace_near line 11335
  633. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerFirstSource line 11344
  634. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerFirstSource_zero_near line 11348
  635. structure OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData line 11386
  636. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.column line 11401
  637. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedColumn line 11406
  638. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.operatorColumn line 11411
  639. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalized_initial line 11420
  640. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalParametrixData line 11429
  641. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedGram_contDiff line 11494
  642. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_fderiv_zero_of_partial line 11508
  643. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedFirst line 11522
  644. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedTail line 11527
  645. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signed_amplitude_regular line 11539
  646. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedFirst_continuous line 11546
  647. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedFirst_regular line 11551
  648. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedFirst_compact line 11557
  649. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedFirst_zero line 11566
  650. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedFirst_fderiv_zero line 11570
  651. theorem OAI.PositiveEinsteinFour.Geometry.heatMatrixScalarOperator_signed_trace line 11603
  652. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.first_amplitude_signed_scalar line 11632
  653. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.second_amplitude_signature_polynomial line 11653
  654. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.second_amplitude_signature_density line 11665
  655. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.first_amplitude_trace_radial line 11690
  656. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.first_amplitude_trace_radial line 11700
  657. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerFirstAmplitude line 11710
  658. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerFirstAmplitude_radial line 11715
  659. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerFirstAmplitude_zero_near line 11749
  660. def OAI.PositiveEinsteinFour.Geometry.heatFamilySignedFirst line 11775
  661. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilySignedFirst_regular line 11779
  662. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.signedFirst_family line 11793
  663. theorem OAI.PositiveEinsteinFour.Geometry.heatUniformSignedFirst_quadratic line 11808
  664. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeTensor_norm_sq line 11857
  665. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeL2_norm_le line 11892
  666. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneColumn line 11933
  667. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneTimeColumn line 11938
  668. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneOperatorColumn line 11943
  669. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneResidual line 11952
  670. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalOneWeakData line 11956
  671. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneWeakEvolution line 11994
  672. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedTail_continuous line 12035
  673. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedTail_bound line 12067
  674. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedTail_zero line 12080
  675. structure OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData line 12109
  676. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatScalarChartData line 12123
  677. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.function line 12148
  678. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.function_regular line 12151
  679. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.column line 12161
  680. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.laplacianColumn line 12165
  681. def OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.parametrixData line 12191
  682. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.parametrixData_cutoff line 12212
  683. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.parametrixData_source line 12215
  684. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.parametrixData_generator line 12221
  685. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage_congr_germ line 12250
  686. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCoefficient_congr_germ line 12269
  687. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.amplitude_companion_germ line 12298
  688. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.eulerFirst_zero_near line 12308
  689. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_zero line 12330
  690. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_finite_sum line 12334
  691. def OAI.PositiveEinsteinFour.Geometry.heatOneMatrixScalarOperator line 12351
  692. theorem OAI.PositiveEinsteinFour.Geometry.heatOneMatrixScalarOperator_trace line 12355
  693. theorem OAI.PositiveEinsteinFour.Geometry.heatMatrixScalarOperator_trace line 12361
  694. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerFirst_scalar_operator_zero line 12372
  695. def OAI.PositiveEinsteinFour.Geometry.heatFamilySignedTail line 12426
  696. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilySignedTail_continuous line 12438
  697. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilySignedTail_bound line 12470
  698. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.signedTail_family line 12490
  699. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeTensor_L2_realization line 12531
  700. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeL2_norm_sq_integral line 12549
  701. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeL2_norm_sq_le_integral line 12632
  702. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.timeColumn line 12709
  703. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.residual line 12714
  704. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.residual_eq line 12722
  705. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.residual_norm_le line 12737
  706. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalGlobalResidual line 12751
  707. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCutoffParametrix_initial_local line 12776
  708. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.one_initial line 12814
  709. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedColumn line 12844
  710. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.one_normalized_initial line 12848
  711. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_second_partial_eq_fderiv line 12877
  712. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedGram_scalar_sub line 12886
  713. theorem OAI.PositiveEinsteinFour.Geometry.heat_actual_potential_symmetric line 12902
  714. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.first_amplitude_signed_gram line 12913
  715. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedFirst_second line 12922
  716. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signedFirst_hessian_trace line 12940
  717. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatScalarAdaptedChart line 12976
  718. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalScalarLift_mul line 13063
  719. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.column_pairing line 13082
  720. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalizedColumn line 13109
  721. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.chart_zero line 13114
  722. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.column_initial line 13120
  723. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalizedColumn_initial line 13137
  724. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.scalar_laplacian_local line 13168
  725. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.column_laplacian_local line 13200
  726. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatActualUniformParametrix line 13234
  727. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.second_amplitude_center line 13272
  728. def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerSecondAmplitude line 13298
  729. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.eulerSecondAmplitude_center line 13303
  730. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeTensor_inner line 13363
  731. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeL2_inner_integral line 13396
  732. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.column_growth line 13476
  733. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.normalizedColumn_growth line 13501
  734. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneColumn_growth line 13533
  735. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedColumn_growth line 13558
  736. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.one_eigen_evolution line 13587
  737. def OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.oneNormalizedResidual line 13605
  738. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.one_normalized_eigen_evolution line 13609
  739. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalOneEvolution line 13624
  740. def OAI.PositiveEinsteinFour.Geometry.heatNormalMatrixPolynomial line 13666
  741. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMatrixPolynomial_component line 13670
  742. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMatrixPolynomial_signed line 13678
  743. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signed_reduced_gaussian_limit line 13687
  744. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.signed_gaussian_limit line 13714
  745. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.operator_pairing line 13749
  746. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalParametrixData.weak_evolution line 13763
  747. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.column_norm_sq_integral line 13813
  748. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.polynomial line 13839
  749. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.cutoff_gaussian line 13843
  750. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.polynomial_weight_bound line 13849
  751. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.square_integral_bound line 13872
  752. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.column_growth line 13901
  753. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalizedColumn_growth line 13919
  754. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.normalizedColumn_gaussian_integral line 13928
  755. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.timeAmplitude line 13969
  756. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.timeAmplitude_regular line 13972
  757. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.timeAmplitude_support line 13987
  758. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.timeAmplitude_eq line 13990
  759. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.timeFunction line 13996
  760. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.timeFunction_regular line 13999
  761. def OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.timeColumn line 14010
  762. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.timeColumn_pairing line 14014
  763. theorem OAI.PositiveEinsteinFour.Geometry.HeatScalarChartData.column_weak_deriv line 14038