OAI/Geometry/EinsteinFour/HodgeTheory08.lean

GitHub source file

559 declarations, 0 contain sorry, 0 declared as axioms

Uniform O(t) control of the cutoff error on all normal coordinates.

  1. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatScaledCommutator_bounded line 35
  2. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatScaledCommutator_gaussian_bound line 62
  3. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_differentiable line 110
  4. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_sum_four line 122
  5. def OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantFlux line 139
  6. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantFlux_derivative line 144
  7. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_germ line 183
  8. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantOperator_germ line 190
  9. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantOperator_zero_of_locally_zero line 204
  10. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_mul_contDiff_of_tsupport line 235
  11. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_pairing_integrable line 246
  12. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_pairing_global line 268
  13. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_partial_integral_zero line 303
  14. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_green_of_pairing line 311
  15. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_pairing_contDiff line 326
  16. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_pairing_compact line 336
  17. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_green line 345
  18. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_metric_pairing_symm line 380
  19. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_potential_pairing_symm line 391
  20. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneOperator_germ line 416
  21. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneOperator_zero_of_locally_zero line 425
  22. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_germ line 437
  23. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantOperator_germ line 444
  24. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantOperator_zero_of_locally_zero line 458
  25. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_norm_sqrt_smul_sq line 487
  26. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_vanishing_scaled_limit line 491
  27. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_vanishing_quadratic_bound line 526
  28. def OAI.PositiveEinsteinFour.Geometry.heatCompactTensorLift line 580
  29. theorem OAI.PositiveEinsteinFour.Geometry.heatCompactTensorLift_support line 585
  30. theorem OAI.PositiveEinsteinFour.Geometry.heatCompactTensorLift_tsupport line 595
  31. theorem OAI.PositiveEinsteinFour.Geometry.heatCompactTensorLift_continuous line 602
  32. theorem OAI.PositiveEinsteinFour.Geometry.heatCompactTensorLift_skew line 623
  33. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyWeightedAverage_slice line 651
  34. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.amplitude_slice line 656
  35. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalar_compact_jet_bound line 707
  36. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.amplitude_compact_bound line 721
  37. def OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.lastCoefficient line 735
  38. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.lastCoefficient_regular line 739
  39. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.lastCoefficient_compact_bound line 748
  40. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneOperator_slice line 781
  41. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalConnectionOperator_eq line 831
  42. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalBundleParametrix_time_differentiable line 864
  43. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalBundleParametrix_space_regular line 871
  44. def OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffParametrix line 879
  45. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffParametrix_residual_identity line 884
  46. theorem OAI.PositiveEinsteinFour.Geometry.heat_hodgeMatrix_symmetric line 925
  47. theorem OAI.PositiveEinsteinFour.Geometry.heat_signed_skew_trace line 929
  48. theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnectionMatrix_signed_trace line 939
  49. theorem OAI.PositiveEinsteinFour.Geometry.heat_actual_potential_signed_trace line 946
  50. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.first_amplitude_signed_trace line 966
  51. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_quadratic_bound_of_hessian line 991
  52. theorem OAI.PositiveEinsteinFour.Geometry.heat_partial_finite_sum line 1032
  53. theorem OAI.PositiveEinsteinFour.Geometry.heat_partial_second_finite_sum line 1039
  54. def OAI.PositiveEinsteinFour.Geometry.heatSixPartial line 1059
  55. theorem OAI.PositiveEinsteinFour.Geometry.heat_trace_product_second_zero line 1062
  56. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.connection_square_second line 1100
  57. theorem OAI.PositiveEinsteinFour.Geometry.heat_twoForm_covariant_tensor line 1140
  58. theorem OAI.PositiveEinsteinFour.Geometry.heat_fourCovariant_congr line 1161
  59. theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_one line 1187
  60. theorem OAI.PositiveEinsteinFour.Geometry.exterior_second_zero line 1196
  61. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormExterior_closed line 1215
  62. def OAI.PositiveEinsteinFour.Geometry.scalarHeatDiagonal line 1257
  63. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatColumn_norm_square line 1260
  64. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatDiagonal_series line 1279
  65. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatDiagonal_integral line 1286
  66. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenbasis_apply line 1334
  67. def OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatLiftSource line 1338
  68. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatLiftSource_resolvent line 1342
  69. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatWeight_half_sq line 1348
  70. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatLiftWeight_bound line 1354
  71. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_series line 1360
  72. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatLiftSource_eigen line 1374
  73. def OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatDerivative line 1388
  74. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatDerivative_eigen line 1392
  75. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatDerivative_series line 1402
  76. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarBaseL2_one_ne_zero line 1443
  77. theorem OAI.PositiveEinsteinFour.Geometry.scalarBase_fixed_space_eq_span line 1455
  78. theorem OAI.PositiveEinsteinFour.Geometry.scalarBase_fixed_finrank line 1478
  79. theorem OAI.PositiveEinsteinFour.Geometry.scalar_minimum_H1_source line 1508
  80. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_framed line 1574
  81. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_component line 1599
  82. def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferentialField line 1650
  83. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantField_derivative_framed line 1654
  84. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferentialField_framed line 1661
  85. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferentialField_component line 1668
  86. def OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamDensity line 1695
  87. theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamDensity_eq_frame line 1699
  88. theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.continuous_framedDeRhamDensity line 1711
  89. theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.continuous_deRhamDensity line 1729
  90. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDeRhamEnergy_eq_base line 1745
  91. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDeRhamEnergy_eq_zero_iff line 1754
  92. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFramedValue_product line 1796
  93. theorem OAI.PositiveEinsteinFour.Geometry.scalarGradient_smoothScalarProduct line 1807
  94. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFramedCovariantDerivative_product line 1821
  95. def OAI.PositiveEinsteinFour.Geometry.scalarDifferentialFiber line 1845
  96. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodifferential_product line 1848
  97. def OAI.PositiveEinsteinFour.Geometry.twoFormShiftedHodgeCompact line 1892
  98. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedHodgeCompact_compact line 1895
  99. def OAI.PositiveEinsteinFour.Geometry.twoFormShiftedHodge line 1898
  100. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedHodge_inner line 1901
  101. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedHodge_eq_zero line 1911
  102. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedHodge_injective line 1920
  103. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedHodge_surjective line 1927
  104. def OAI.PositiveEinsteinFour.Geometry.twoFormShiftedHodgeEquiv line 1943
  105. def OAI.PositiveEinsteinFour.Geometry.twoFormShiftedSolution line 1948
  106. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedSolution_equation line 1951
  107. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedSolution_weak line 1955
  108. def OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent line 1961
  109. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_compact line 1964
  110. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_selfAdjoint line 1968
  111. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_nonneg line 1985
  112. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_injective line 1997
  113. theorem OAI.PositiveEinsteinFour.Geometry.exists_weakHodgePoisson line 2026
  114. theorem OAI.PositiveEinsteinFour.Geometry.weakHodgePoisson_unique line 2057
  115. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantOperator_divergence line 2092
  116. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_covariant_divergence_green line 2163
  117. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_contDiffAt line 2205
  118. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantFlux_contDiffAt line 2215
  119. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_support line 2228
  120. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantFlux_support line 2246
  121. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantFlux_compact line 2260
  122. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_bilinear_coordinates line 2284
  123. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_bilinear_integral line 2301
  124. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_second_order_limit line 2317
  125. def OAI.PositiveEinsteinFour.Geometry.fourHeatOneScaledCommutator line 2374
  126. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneScaledCommutator_identity line 2383
  127. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneScaledCommutator_continuous line 2425
  128. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneScaledCommutator_zero_of_locally_const line 2459
  129. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneScaledCommutator_bounded line 2475
  130. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneScaledCommutator_gaussian_bound line 2502
  131. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_skew_pairing line 2549
  132. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_pairing line 2564
  133. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_pairing_integrable line 2584
  134. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_pairing_global line 2606
  135. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_pairing_contDiff line 2641
  136. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_pairing_compact line 2651
  137. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_green line 2660
  138. def OAI.PositiveEinsteinFour.Geometry.heatFamilySpatialFDeriv line 2707
  139. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilySpatialFDeriv_slice line 2711
  140. theorem OAI.PositiveEinsteinFour.Geometry.heatFamily_quadratic_bound line 2719
  141. def OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.normalExtension line 2771
  142. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.normalExtension_amplitude line 2806
  143. structure OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients line 2835
  144. def OAI.PositiveEinsteinFour.Geometry.heatFamilyOneCoefficientSequence line 2842
  145. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneCoefficientSequence_contDiff line 2851
  146. def OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.amplitude line 2880
  147. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.amplitude_regular line 2884
  148. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyPolynomial_continuous line 2912
  149. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyPolynomial_partial_continuous line 2923
  150. def OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarOperator line 2954
  151. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarOperator_contDiff line 2959
  152. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarOperator_slice line 2968
  153. def OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarSequence line 2978
  154. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarSequence_contDiff line 2985
  155. def OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.scalarAmplitude line 3007
  156. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.scalarAmplitude_regular line 3010
  157. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.scalarAmplitude_slice line 3018
  158. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalChartMap_source line 3064
  159. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalChartTensor_realization line 3072
  160. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalTensor_L2_realization line 3113
  161. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffParametrix_residual_zero line 3167
  162. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffParametrix_initial line 3206
  163. theorem OAI.PositiveEinsteinFour.Geometry.heatOneForm_covariant_skew line 3254
  164. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneFormValue line 3269
  165. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneFormValue_regular line 3274
  166. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneForm_covariant line 3289
  167. def OAI.PositiveEinsteinFour.Geometry.heatNormalOneOperatorAmplitude line 3329
  168. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneOperatorAmplitude_regular line 3334
  169. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneOperatorAmplitude_support line 3347
  170. def OAI.PositiveEinsteinFour.Geometry.heatMatrixScalarOperator line 3382
  171. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.second_amplitude_center line 3391
  172. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.second_amplitude_signed_trace line 3418
  173. theorem OAI.PositiveEinsteinFour.Geometry.heatNormal_tensor_first line 3452
  174. theorem OAI.PositiveEinsteinFour.Geometry.heatNormal_tensor_second line 3467
  175. def OAI.PositiveEinsteinFour.Geometry.heatSignedGram line 3527
  176. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedGram_add_left line 3530
  177. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedGram_add_right line 3534
  178. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedGram_smul_left line 3538
  179. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedGram_smul_right line 3543
  180. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedGram_comm line 3547
  181. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedGram_one_left line 3556
  182. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedGram_one_one line 3560
  183. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedGram_polynomial line 3563
  184. instance OAI.PositiveEinsteinFour.Geometry.heatSignedTraceENorm line 3596
  185. def OAI.PositiveEinsteinFour.Geometry.heatSignedTraceLinear line 3600
  186. theorem OAI.PositiveEinsteinFour.Geometry.heatSixPartial_eq_fderiv line 3606
  187. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedTrace_partial line 3617
  188. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedTrace_second line 3628
  189. theorem OAI.PositiveEinsteinFour.Geometry.heatSignedTrace_weightedRadial line 3644
  190. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormExterior_adjoint line 3706
  191. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonic_orthogonal_exact line 3746
  192. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonic_exact_eq_zero line 3754
  193. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_derivative_green line 3783
  194. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_ricci_commutator line 3813
  195. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_rate_weight_summable line 3874
  196. def OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatRealTerm line 3900
  197. def OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatRealDerivativeTerm line 3905
  198. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatRealDerivativeTerm_bound line 3910
  199. def OAI.PositiveEinsteinFour.Geometry.scalarHeatH1Lift line 3952
  200. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatH1Lift_value line 3955
  201. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatH1Lift_smooth line 3959
  202. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatH1Lift_eigen line 3965
  203. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatToContinuous_add line 3999
  204. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatColumn_add line 4007
  205. def OAI.PositiveEinsteinFour.Geometry.scalarHeatKernel line 4015
  206. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatKernel_pairing line 4019
  207. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatKernel_symm line 4025
  208. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatKernel_diagonal line 4030
  209. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatKernel_L2 line 4035
  210. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatKernel_action line 4044
  211. theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_minimum_continuous line 4082
  212. theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_minimum_positive_continuous line 4127
  213. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDeRhamEnergy_hodge line 4165
  214. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicTwoForms_hodge line 4180
  215. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicHodge line 4186
  216. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicHodge_involutive line 4192
  217. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicPositive line 4201
  218. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicNegative line 4205
  219. instance OAI.PositiveEinsteinFour.Geometry.smoothHarmonicPositive_finite line 4209
  220. instance OAI.PositiveEinsteinFour.Geometry.smoothHarmonicNegative_finite line 4214
  221. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicPlus line 4219
  222. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicMinus line 4226
  223. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonic_decomposition line 4234
  224. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodiffTensor_squareNorm line 4258
  225. def OAI.PositiveEinsteinFour.Geometry.twoFormCodiffDensity line 4272
  226. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodiffDensity_eq_frame line 4275
  227. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodiffDensity_continuous line 4281
  228. theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamDensity_hodge line 4285
  229. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferentialField_derivative line 4327
  230. def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDDelta line 4351
  231. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDDelta_component line 4354
  232. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDDelta_closed line 4364
  233. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferentialField_add line 4387
  234. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferentialField_smul line 4400
  235. def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferentialLinear line 4412
  236. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_norm_le line 4439
  237. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_pos line 4451
  238. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_eigenvalue line 4466
  239. theorem OAI.PositiveEinsteinFour.Geometry.twoFormResolvent_eigenvector_weak line 4480
  240. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeEquation_rough_iff line 4529
  241. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeEquation_smooth_test line 4547
  242. theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeakHarmonic_rough line 4560
  243. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantFlux_contDiff line 4583
  244. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_scalar line 4622
  245. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_differentiable line 4642
  246. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_sum_four line 4654
  247. def OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantFlux line 4671
  248. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantFlux_derivative line 4676
  249. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantOperator_divergence line 4698
  250. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_contDiffAt line 4752
  251. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantFlux_contDiffAt line 4762
  252. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_support line 4775
  253. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantFlux_support line 4793
  254. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantFlux_compact line 4807
  255. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_covariant_divergence_green line 4815
  256. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_half_tendsto line 4856
  257. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_square_first_order_limit line 4867
  258. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_square_amplitude_integrable line 4883
  259. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_signed_gaussian_limit line 4894
  260. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_potential_pairing_integrable line 4945
  261. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantOperator_weighted_green line 4964
  262. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatActualAmplitudeFamily line 5048
  263. def OAI.PositiveEinsteinFour.Geometry.heatFamilyCommutator line 5137
  264. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyCommutator_continuous line 5142
  265. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyCommutator_bounded line 5186
  266. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyCommutator_gaussian_bound line 5213
  267. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.amplitude_slice line 5255
  268. def OAI.PositiveEinsteinFour.Geometry.heatFamilyOneCommutator line 5306
  269. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneCommutator_continuous line 5311
  270. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneCommutator_bounded line 5355
  271. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneCommutator_gaussian_bound line 5382
  272. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.amplitude_compact_bound line 5424
  273. def OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.lastCoefficient line 5438
  274. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.lastCoefficient_regular line 5442
  275. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.lastCoefficient_compact_bound line 5451
  276. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatFamilyOneCoefficients line 5484
  277. def OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarCommutator line 5525
  278. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarCommutator_continuous line 5530
  279. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarCommutator_bounded line 5572
  280. theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarCommutator_gaussian_bound line 5591
  281. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.scalarAmplitude_compact_bound line 5633
  282. def OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.scalarLastCoefficient line 5646
  283. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.scalarLastCoefficient_regular line 5650
  284. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.scalarLastCoefficient_compact_bound line 5656
  285. theorem OAI.PositiveEinsteinFour.Geometry.heat_continuous_mul_of_tsupport_subset line 5682
  286. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoffParametrix_initial_local line 5698
  287. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.actual_rough_components_near line 5751
  288. theorem OAI.PositiveEinsteinFour.Geometry.heat_oneForm_covariant_component line 5826
  289. theorem OAI.PositiveEinsteinFour.Geometry.heat_oneForm_covariant_second line 5833
  290. structure OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember line 5874
  291. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatUniformNormalFamily line 5898
  292. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_closed_second_symmetric line 6028
  293. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_trace_second_zero line 6045
  294. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_harmonic_rough line 6072
  295. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_derivative_integral_zero line 6110
  296. theorem OAI.PositiveEinsteinFour.Geometry.oneFormDivergence_mean_zero line 6126
  297. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatContinuous_eigen_split line 6164
  298. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatContinuous_eigen_bound line 6174
  299. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatKernel_hasSum line 6188
  300. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatKernel_continuous line 6205
  301. def OAI.PositiveEinsteinFour.Geometry.scalarHeatRealColumn line 6259
  302. def OAI.PositiveEinsteinFour.Geometry.scalarHeatRealDiagonal line 6262
  303. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatRealColumn_pos line 6265
  304. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatRealDiagonal_columns line 6269
  305. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatRealTerm_derivative line 6303
  306. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatRealTerm_hasSum line 6321
  307. theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_hasDerivAt line 6327
  308. theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_minimum_positive_C1 line 6374
  309. theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_minimum_positive_smooth line 6447
  310. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferential_continuous line 6522
  311. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodiffProduct_integrable line 6528
  312. def OAI.PositiveEinsteinFour.Geometry.twoFormCodiffPairing line 6536
  313. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodiffPairing_comm line 6540
  314. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodiffPairing_add_left line 6547
  315. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodiffPairing_smul_left line 6553
  316. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodiffPairing_self line 6559
  317. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDeRhamEnergy_codiff line 6574
  318. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDDelta_pairing line 6584
  319. theorem OAI.PositiveEinsteinFour.Geometry.mass_pairing line 6624
  320. theorem OAI.PositiveEinsteinFour.Geometry.energy_pairing line 6634
  321. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramVectorL2_mass line 6645
  322. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramNablaL2_energy line 6681
  323. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_symmetric line 6749
  324. abbrev OAI.PositiveEinsteinFour.Geometry.TwoFormSpectralValue line 6753
  325. abbrev OAI.PositiveEinsteinFour.Geometry.TwoFormSpectralSpace line 6756
  326. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectralValue_bounds line 6759
  327. instance OAI.PositiveEinsteinFour.Geometry.twoFormSpectralSpaceFinite line 6763
  328. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectral_orthogonal_bot line 6769
  329. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectral_total line 6777
  330. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectral_isHilbertSum line 6783
  331. def OAI.PositiveEinsteinFour.Geometry.twoFormSpectralEquiv line 6791
  332. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectral_sum line 6796
  333. def OAI.PositiveEinsteinFour.Geometry.fourHeatEnergyDensity line 6823
  334. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_flux_pairing line 6830
  335. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatEnergyDensity_symm_at line 6848
  336. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_potential_pairing_integrable line 6888
  337. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantOperator_weighted_green line 6907
  338. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_metric_pairing_symm line 6971
  339. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_potential_pairing_symm line 6982
  340. def OAI.PositiveEinsteinFour.Geometry.fourHeatOneEnergyDensity line 6994
  341. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_flux_pairing line 7001
  342. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneEnergyDensity_symm_at line 7019
  343. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_flux_pairing_swap line 7043
  344. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantFlux_contDiff line 7069
  345. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_left_integrable line 7092
  346. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_energy_integral line 7120
  347. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_signed_gaussian_bound line 7166
  348. def OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.normalExtension line 7237
  349. theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilyOneCoefficients.normalExtension_amplitude line 7259
  350. theorem OAI.PositiveEinsteinFour.Geometry.heat_smoothHodge_frameValue line 7298
  351. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.actual_bundle_operator_near line 7312
  352. def OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarCutoff line 7381
  353. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarCutoff_regular line 7385
  354. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarCutoff_support line 7389
  355. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarCutoff_initial line 7393
  356. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarCutoff_pairing_deriv line 7416
  357. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.transport line 7467
  358. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_valueSquare_integrable line 7543
  359. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_secondPair_integrable line 7550
  360. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_harmonic_component_integral line 7564
  361. theorem OAI.PositiveEinsteinFour.Geometry.oneForm_harmonic_eq_zero line 7598
  362. theorem OAI.PositiveEinsteinFour.Geometry.scalar_smooth_laplacian_of_weak line 7635
  363. theorem OAI.PositiveEinsteinFour.Geometry.scalarHeat_laplacian line 7663
  364. theorem OAI.PositiveEinsteinFour.Geometry.scalar_oneForm_direction_green line 7708
  365. theorem OAI.PositiveEinsteinFour.Geometry.scalar_oneForm_adjoint line 7733
  366. theorem OAI.PositiveEinsteinFour.Geometry.actual_scalar_subcritical_bound line 7783
  367. theorem OAI.PositiveEinsteinFour.Geometry.actual_sharpScalarSobolev line 7798
  368. theorem OAI.PositiveEinsteinFour.Geometry.actual_gurskyLeBrunGap line 7804
  369. def OAI.PositiveEinsteinFour.Geometry.twoFormLocalTestH1 line 7842
  370. def OAI.PositiveEinsteinFour.Geometry.twoFormLocalPairing line 7844
  371. theorem OAI.PositiveEinsteinFour.Geometry.twoFormLocalPairing_continuous line 7853
  372. theorem OAI.PositiveEinsteinFour.Geometry.twoFormLocalPairing_smooth line 7862
  373. theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1_localPairing line 7876
  374. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRough_localEquation line 7888
  375. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_localEquation line 7895
  376. def OAI.PositiveEinsteinFour.Geometry.twoFormSpectralMultiplier line 7923
  377. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectralMultiplier_coordinate line 7939
  378. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectralMultiplier_norm line 7949
  379. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectralMultiplier_inner line 7966
  380. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectralMultiplier_selfAdjoint line 7977
  381. structure OAI.PositiveEinsteinFour.ClassicalOrientedData line 8014
  382. def OAI.PositiveEinsteinFour.ClassicalOrientedInputs line 8021
  383. theorem OAI.PositiveEinsteinFour.ClassicalOrientedInputs.toRemaining line 8028
  384. structure OAI.PositiveEinsteinFour.ClassicalClassificationInputs line 8040
  385. theorem OAI.PositiveEinsteinFour.classificationOn_of_classical_inputs line 8045
  386. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalar_eq_zero_of_square_integral line 8074
  387. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferential_gradient_orthogonal line 8088
  388. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferential_divergence line 8100
  389. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_flux_pairing_swap line 8128
  390. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_left_integrable line 8170
  391. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_energy_integral line 8198
  392. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_compact_flux_green line 8244
  393. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOne_potential_pairing_swap line 8270
  394. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantOperator_compact_adjoint line 8289
  395. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.rough_pullback_at line 8419
  396. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.actual_tensor_rough_at line 8449
  397. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.actual_rough_components_at line 8469
  398. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.actual_bundle_operator_at line 8527
  399. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.rough_pullback_uniform_near line 8597
  400. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.actual_tensor_rough_uniform_near line 8628
  401. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.actual_rough_components_uniform_near line 8645
  402. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.actual_bundle_operator_uniform_near line 8704
  403. structure OAI.PositiveEinsteinFour.Geometry.HeatCommonEulerMember line 8767
  404. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatUniformEulerFamily line 8779
  405. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.amplitude_family line 8916
  406. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.amplitude_transport line 8923
  407. theorem OAI.PositiveEinsteinFour.Geometry.HeatCommonNormalMember.parametrix_residual line 8941
  408. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothScalar_primitive line 9000
  409. def OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeLaplacian line 9046
  410. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeLaplacian_apply line 9050
  411. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferential_pairing line 9060
  412. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferential_pairing line 9072
  413. def OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeEnergy line 9080
  414. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeLaplacian_pairing line 9084
  415. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeEnergy_comm line 9095
  416. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeLaplacian_selfAdjoint line 9103
  417. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeEnergy_nonneg line 9111
  418. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeLaplacian_nonneg line 9115
  419. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatRate line 9141
  420. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatRate_nonneg line 9144
  421. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatRate_eq_zero line 9149
  422. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatWeight line 9154
  423. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatWeight_bound line 9158
  424. def OAI.PositiveEinsteinFour.Geometry.twoFormHeat line 9164
  425. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_coordinate line 9168
  426. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_zero line 9174
  427. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_add line 9182
  428. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_contraction line 9194
  429. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_selfAdjoint line 9199
  430. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_nonneg line 9203
  431. theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2GramValue_H1 line 9234
  432. theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2_localTest line 9250
  433. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRough_localL2Equation line 9281
  434. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_localL2Equation line 9296
  435. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectralValue_abs_le line 9332
  436. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_eq_multiplier line 9337
  437. theorem OAI.PositiveEinsteinFour.Geometry.twoFormShiftedResolvent_coordinate line 9349
  438. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectralMultiplier_sub_norm_sq line 9376
  439. theorem OAI.PositiveEinsteinFour.Geometry.twoFormSpectralMultiplier_tendsto line 9395
  440. theorem OAI.PositiveEinsteinFour.Geometry.weylRoot_weighted_moment line 9461
  441. theorem OAI.PositiveEinsteinFour.Geometry.actual_weyl_gap_limiting_inequality line 9485
  442. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_compact_flux_green line 9549
  443. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_potential_pairing_swap line 9575
  444. theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalOperatorChart line 9615
  445. def OAI.PositiveEinsteinFour.Geometry.smoothH1Codifferential line 9674
  446. theorem OAI.PositiveEinsteinFour.Geometry.smoothH1Codifferential_norm_sq line 9683
  447. theorem OAI.PositiveEinsteinFour.Geometry.smoothH1Codifferential_norm_le line 9695
  448. def OAI.PositiveEinsteinFour.Geometry.smoothH1CodifferentialCLM line 9734
  449. def OAI.PositiveEinsteinFour.Geometry.twoFormH1Codifferential line 9739
  450. theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1Codifferential_smooth line 9742
  451. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarFirstJet_injective line 9770
  452. def OAI.PositiveEinsteinFour.Geometry.scalarFirstJetRangeEquiv line 9777
  453. def OAI.PositiveEinsteinFour.Geometry.scalarFirstJetRangeInclusion line 9781
  454. theorem OAI.PositiveEinsteinFour.Geometry.scalarFirstJetRangeInclusion_dense line 9789
  455. theorem OAI.PositiveEinsteinFour.Geometry.scalarFirstJetRangeInclusion_equiv line 9800
  456. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferential_dirichlet line 9804
  457. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferential_norm_le line 9812
  458. def OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferentialL2 line 9823
  459. def OAI.PositiveEinsteinFour.Geometry.scalarFirstJetDifferential line 9832
  460. theorem OAI.PositiveEinsteinFour.Geometry.scalarFirstJetDifferential_equiv line 9836
  461. theorem OAI.PositiveEinsteinFour.Geometry.scalarFirstJetDifferential_norm_le line 9845
  462. def OAI.PositiveEinsteinFour.Geometry.scalarFirstJetDifferentialCLM line 9852
  463. def OAI.PositiveEinsteinFour.Geometry.scalarH1Differential line 9858
  464. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Differential_range line 9862
  465. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Differential_smooth line 9872
  466. abbrev OAI.PositiveEinsteinFour.Geometry.smoothClosedOneForms line 9903
  467. def OAI.PositiveEinsteinFour.Geometry.smoothExactOneForms line 9909
  468. abbrev OAI.PositiveEinsteinFour.Geometry.OneFormDeRhamCohomology line 9913
  469. theorem OAI.PositiveEinsteinFour.Geometry.smoothExactOneForms_eq_top line 9919
  470. theorem OAI.PositiveEinsteinFour.Geometry.oneFormDeRhamCohomology_eq_zero line 9927
  471. theorem OAI.PositiveEinsteinFour.Geometry.oneFormDeRhamCohomology_subsingleton line 9935
  472. theorem OAI.PositiveEinsteinFour.Geometry.oneFormDeRhamCohomology_finrank line 9940
  473. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeLaplacian_eq_zero line 9969
  474. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormHodgeLaplacian_injective line 9998
  475. theorem OAI.PositiveEinsteinFour.Geometry.oneFormDivergence_gradient line 10026
  476. theorem OAI.PositiveEinsteinFour.Geometry.smoothOneForm_Weitzenbock line 10057
  477. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatWeight_continuous line 10104
  478. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_continuous line 10110
  479. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_tendsto_zero_time line 10119
  480. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeat_joint_continuous line 10126
  481. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatLiftWeight_bound line 10178
  482. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatLiftSource line 10203
  483. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatLiftSource_resolvent line 10208
  484. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatLift line 10221
  485. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatLift_value line 10225
  486. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatLift_weak line 10229
  487. theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeitzenbockPotential_smooth line 10261
  488. theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartValue_potential line 10268
  489. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotential_chart_pair line 10304
  490. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotential_chart_memSobolev_one line 10363
  491. def OAI.PositiveEinsteinFour.Geometry.twoFormScalarTestL2 line 10390
  492. theorem OAI.PositiveEinsteinFour.Geometry.twoFormMassPair_scalarTest line 10405
  493. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEnergyPair_scalarTest line 10413
  494. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRough_scalarWeakEquation line 10440
  495. theorem OAI.PositiveEinsteinFour.Geometry.twoForm_smooth_gram_integer line 10496
  496. theorem OAI.PositiveEinsteinFour.Geometry.twoForm_smooth_source_integer line 10523
  497. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantOperator_compact_adjoint line 10557
  498. theorem OAI.PositiveEinsteinFour.Geometry.heat_covariantField_chart line 10684
  499. theorem OAI.PositiveEinsteinFour.Geometry.oneFormSecond_coordinates line 10704
  500. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneRoughTrace_as_actual line 10715
  501. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneTensor_rough_at line 10740
  502. theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexL2_compact_inner_derivative line 10784
  503. theorem OAI.PositiveEinsteinFour.Geometry.scalar_divergence_corrected_flux line 10807
  504. theorem OAI.PositiveEinsteinFour.Geometry.scalarC1_compact_test line 10845
  505. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGram_weak_partial line 10876
  506. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatPowerWeight_bound line 10916
  507. def OAI.PositiveEinsteinFour.Geometry.twoFormHeatPowerSource line 10947
  508. theorem OAI.PositiveEinsteinFour.Geometry.twoFormResolvent_power_coordinate line 10953
  509. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHeatPowerSource_resolvent line 10965
  510. def OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalCoefficient line 11000
  511. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalCoefficient_smooth line 11007
  512. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFluxPair_basis_test line 11013
  513. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneValue_as_actual line 11064
  514. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneRough_components_at line 11077
  515. theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.actual_one_operator_at line 11102
  516. def OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalTest line 11160
  517. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalTest_smooth line 11164
  518. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalTest_compact line 11169
  519. def OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalDerivativeTestL2 line 11173
  520. def OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalDivergenceTestL2 line 11178
  521. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalFlux_integrationByParts line 11184
  522. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRough_principalWeakEquation line 11250
  523. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalTest_support line 11312
  524. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalTest_remove_cutoff line 11317
  525. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalDivergence_value line 11328
  526. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalDivergenceTestL2_coe line 11356
  527. def OAI.PositiveEinsteinFour.Geometry.twoFormWeightedComponentL2 line 11410
  528. theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeightedComponent_H1 line 11414
  529. theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeightedComponent_coe line 11421
  530. theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeightedComponent_operator_pairing line 11439
  531. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRough_weightedWeakEquation line 11488
  532. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRough_weighted_H2 line 11541
  533. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRough_actual_local_H2 line 11581
  534. theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeightedComponent_rescaled_coe line 11633
  535. theorem OAI.PositiveEinsteinFour.Geometry.twoFormH2_unweight_unscale line 11659
  536. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRough_H2_representative line 11727
  537. theorem OAI.PositiveEinsteinFour.Geometry.twoFormInteger_unweight_unscale line 11798
  538. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGram_cutoff_distribution line 11866
  539. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGram_cutoff_memSobolev line 11911
  540. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRough_common_H2 line 11949
  541. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGram_cutoff_sum line 11987
  542. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGram_order_of_six line 12058
  543. theorem OAI.PositiveEinsteinFour.Geometry.twoFormRough_inner_H2 line 12077
  544. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramConnection_memSobolev_two line 12129
  545. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramDerivativeCorrection_memSobolev_two line 12144
  546. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCovariant_memSobolev_one line 12156
  547. theorem OAI.PositiveEinsteinFour.Geometry.twoForm_local_sobolev_assembly line 12201
  548. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPair_memSobolev_two line 12273
  549. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFluxCorrection_memSobolev_two line 12307
  550. theorem OAI.PositiveEinsteinFour.Geometry.twoFormFluxCorrection_H1_derivatives line 12322
  551. theorem OAI.PositiveEinsteinFour.Geometry.twoFormInnerNabla_component_H1 line 12372
  552. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonicDivergenceSource_H1 line 12382
  553. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPair_memSobolev_integer line 12434
  554. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramConnection_memSobolev_integer line 12487
  555. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramDerivativeCorrection_memSobolev_integer line 12502
  556. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCovariant_memSobolev_integer line 12513
  557. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_principalWeakH1 line 12577
  558. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonic_weightedWeakH1 line 12629
  559. theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotential_local_integer line 12692