OAI/Geometry/Relativity/CKS/HeatBase.lean

GitHub source file

209 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSSphericalHarmonics.Poly line 10
  2. def OAI.CKSSphericalHarmonics.radiusSq line 12
  3. def OAI.CKSSphericalHarmonics.laplacian line 14
  4. def OAI.CKSSphericalHarmonics.radialHarmonicSpan line 17
  5. lemma OAI.CKSSphericalHarmonics.laplacian_apply line 22
  6. lemma OAI.CKSSphericalHarmonics.radiusSq_homogeneous line 26
  7. lemma OAI.CKSSphericalHarmonics.pderiv_radiusSq line 31
  8. lemma OAI.CKSSphericalHarmonics.laplacian_homogeneous line 34
  9. lemma OAI.CKSSphericalHarmonics.laplacian_radiusSq_mul line 41
  10. lemma OAI.CKSSphericalHarmonics.laplacian_radiusSq_mul_homogeneous line 49
  11. lemma OAI.CKSSphericalHarmonics.laplacian_radial_power line 56
  12. lemma OAI.CKSSphericalHarmonics.radialHarmonicSpan_le_homogeneous line 82
  13. lemma OAI.CKSSphericalHarmonics.harmonic_mem_radialHarmonicSpan line 90
  14. lemma OAI.CKSSphericalHarmonics.radialHarmonicSpan_le_map_laplacian line 97
  15. lemma OAI.CKSSphericalHarmonics.laplacian_homogeneous_low line 111
  16. theorem OAI.CKSSphericalHarmonics.harmonic_radial_decomposition line 124
  17. def OAI.CKSSphericalHarmonics.rotation line 144
  18. def OAI.CKSSphericalHarmonics.euler line 147
  19. lemma OAI.CKSSphericalHarmonics.rotation_apply line 149
  20. lemma OAI.CKSSphericalHarmonics.euler_apply line 153
  21. lemma OAI.CKSSphericalHarmonics.euler_homogeneous line 156
  22. lemma OAI.CKSSphericalHarmonics.pderiv_commute line 160
  23. lemma OAI.CKSSphericalHarmonics.laplacian_X_mul line 169
  24. lemma OAI.CKSSphericalHarmonics.laplacian_pderiv line 174
  25. lemma OAI.CKSSphericalHarmonics.laplacian_rotation line 181
  26. lemma OAI.CKSSphericalHarmonics.rotation_homogeneous line 187
  27. lemma OAI.CKSSphericalHarmonics.rotation_casimir line 201
  28. theorem OAI.CKSSphericalHarmonics.harmonic_rotation_eigenvalue line 209
  29. def OAI.CKSSphericalHarmonics.sphereCoordinate line 218
  30. def OAI.CKSSphericalHarmonics.sphereEval line 221
  31. def OAI.CKSSphericalHarmonics.harmonicPolynomials line 223
  32. def OAI.CKSSphericalHarmonics.harmonicSpace line 226
  33. lemma OAI.CKSSphericalHarmonics.sphereEval_X line 229
  34. lemma OAI.CKSSphericalHarmonics.sphereEval_radiusSq line 232
  35. lemma OAI.CKSSphericalHarmonics.polynomialRestrictions_separate line 240
  36. lemma OAI.CKSSphericalHarmonics.radialRestriction_mem_harmonicSpan line 250
  37. lemma OAI.CKSSphericalHarmonics.polynomialRestriction_mem_harmonicSpan line 259
  38. theorem OAI.CKSSphericalHarmonics.spherical_harmonics_dense line 267
  39. instance OAI.CKSSphericalHarmonics.harmonicPolynomials_finite line 278
  40. instance OAI.CKSSphericalHarmonics.harmonicSpace_finite line 283
  41. abbrev OAI.CKSSphericalHarmonics.SphereL2 line 289
  42. def OAI.CKSSphericalHarmonics.toL2 line 291
  43. def OAI.CKSSphericalHarmonics.harmonicL2 line 293
  44. instance OAI.CKSSphericalHarmonics.harmonicL2_finite line 296
  45. def OAI.CKSSphericalHarmonics.harmonicProjection line 300
  46. lemma OAI.CKSSphericalHarmonics.harmonicProjection_norm_le line 303
  47. theorem OAI.CKSSphericalHarmonics.spherical_harmonics_L2_dense line 307
  48. lemma OAI.CKSSphericalHarmonics.toL2_injective line 320
  49. def OAI.CKSSphericalHarmonics.harmonicContinuousEquiv line 323
  50. def OAI.CKSSphericalHarmonics.harmonicCoefficient line 326
  51. lemma OAI.CKSSphericalHarmonics.harmonicCoefficient_mem line 331
  52. lemma OAI.CKSSphericalHarmonics.toL2_harmonicCoefficient line 335
  53. def OAI.CKSSphericalHarmonics.sphereHome line 341
  54. lemma OAI.CKSSphericalHarmonics.sphereHome_val line 346
  55. lemma OAI.CKSSphericalHarmonics.volume_preimage_isometry line 349
  56. lemma OAI.CKSSphericalHarmonics.sphereCone_preimage line 356
  57. theorem OAI.CKSSphericalHarmonics.sphereHome_measurePreserving line 373
  58. def OAI.CKSSphericalHarmonics.planeRotationMap line 382
  59. lemma OAI.CKSSphericalHarmonics.planeRotationMap_apply line 397
  60. lemma OAI.CKSSphericalHarmonics.planeRotationMap_norm line 402
  61. lemma OAI.CKSSphericalHarmonics.planeRotationMap_neg line 413
  62. def OAI.CKSSphericalHarmonics.planeRotation line 427
  63. lemma OAI.CKSSphericalHarmonics.planeRotation_apply line 436
  64. def OAI.CKSSphericalHarmonics.rotatedCoordinate line 440
  65. def OAI.CKSSphericalHarmonics.rotationAction line 445
  66. lemma OAI.CKSSphericalHarmonics.rotationAction_zero line 448
  67. lemma OAI.CKSSphericalHarmonics.rotationAction_apply line 458
  68. lemma OAI.CKSSphericalHarmonics.rotatedCoordinate_hasDerivAt_zero line 474
  69. lemma OAI.CKSSphericalHarmonics.rotationAction_hasDerivAt_zero line 494
  70. def OAI.CKSSphericalHarmonics.sphereIntegral line 514
  71. lemma OAI.CKSSphericalHarmonics.sphereIntegral_apply line 517
  72. lemma OAI.CKSSphericalHarmonics.sphereIntegral_rotationAction line 523
  73. theorem OAI.CKSSphericalHarmonics.sphereIntegral_rotation line 530
  74. lemma OAI.CKSSphericalHarmonics.inner_sphereEval line 542
  75. theorem OAI.CKSSphericalHarmonics.rotation_skew_adjoint line 551
  76. def OAI.CKSSphericalHarmonics.angularLaplacian line 561
  77. lemma OAI.CKSSphericalHarmonics.angularLaplacian_apply line 566
  78. lemma OAI.CKSSphericalHarmonics.rotation_square_symmetric line 570
  79. lemma OAI.CKSSphericalHarmonics.angularLaplacian_symmetric line 575
  80. def OAI.CKSSphericalHarmonics.eigenvalue line 582
  81. lemma OAI.CKSSphericalHarmonics.eigenvalue_injective line 584
  82. lemma OAI.CKSSphericalHarmonics.different_harmonics_inner_zero line 595
  83. theorem OAI.CKSSphericalHarmonics.harmonicL2_orthogonal line 610
  84. lemma OAI.CKSSphericalHarmonics.harmonicL2_orthogonalFamily line 617
  85. theorem OAI.CKSSphericalHarmonics.harmonicHilbertSum line 622
  86. lemma OAI.CKSSphericalHarmonics.harmonicProjection_other line 627
  87. lemma OAI.CKSSphericalHarmonics.harmonicHilbertSum_coefficient line 632
  88. theorem OAI.CKSSphericalHarmonics.harmonicProjections_hasSum line 648
  89. lemma OAI.CKSSphericalHarmonics.rotation_harmonic line 658
  90. lemma OAI.CKSSphericalHarmonics.rotational_energy line 663
  91. lemma OAI.CKSSphericalHarmonics.eigenvalue_nonneg line 678
  92. lemma OAI.CKSSphericalHarmonics.eigenvalue_pos line 679
  93. lemma OAI.CKSSphericalHarmonics.rotation_norm_le line 684
  94. lemma OAI.CKSSphericalHarmonics.sphereEval_rotation_of_zero line 731
  95. lemma OAI.CKSSphericalHarmonics.harmonicSpace_zero_constant line 742
  96. lemma OAI.CKSSphericalHarmonics.angular_kernel_constant line 752
  97. abbrev OAI.CKSSphericalHarmonics.HarmonicBasisIndex line 777
  98. def OAI.CKSSphericalHarmonics.harmonicBasis line 778
  99. lemma OAI.CKSSphericalHarmonics.harmonicL2_exists_polynomial line 780
  100. def OAI.CKSSphericalHarmonics.harmonicBasisPolynomial line 785
  101. lemma OAI.CKSSphericalHarmonics.harmonicBasisPolynomial_spec line 788
  102. lemma OAI.CKSSphericalHarmonics.harmonic_polynomial_basis_expansion line 794
  103. def OAI.CKSSphericalHarmonics.harmonicKernelPolynomial line 807
  104. lemma OAI.CKSSphericalHarmonics.harmonicKernel_rotation line 810
  105. def OAI.CKSSphericalHarmonics.sphereArea line 863
  106. lemma OAI.CKSSphericalHarmonics.sphereArea_pos line 865
  107. lemma OAI.CKSSphericalHarmonics.harmonicKernel_integral line 879
  108. lemma OAI.CKSSphericalHarmonics.harmonicKernel_constant line 890
  109. lemma OAI.CKSSphericalHarmonics.harmonic_coefficients_sq_sum line 905
  110. lemma OAI.CKSSphericalHarmonics.harmonic_sup_norm_le line 913
  111. def OAI.CKSSphericalHarmonics.boundedExponentEquiv line 937
  112. lemma OAI.CKSSphericalHarmonics.restrictDegree_finrank line 945
  113. lemma OAI.CKSSphericalHarmonics.harmonic_dimension_le line 953
  114. lemma OAI.CKSSphericalHarmonics.harmonic_sup_norm_polynomial line 966
  115. def OAI.CKSSphericalHarmonics.rotationWord line 987
  116. lemma OAI.CKSSphericalHarmonics.rotationWord_harmonic line 991
  117. lemma OAI.CKSSphericalHarmonics.rotationWord_L2_norm_le line 998
  118. lemma OAI.CKSSphericalHarmonics.rotationWord_sup_norm_le line 1014
  119. instance OAI.CKSSphericalHarmonics.ambient_finrank line 1040
  120. def OAI.CKSSphericalHarmonics.puncturedSpace line 1042
  121. lemma OAI.CKSSphericalHarmonics.sphere_ne_zero line 1045
  122. lemma OAI.CKSSphericalHarmonics.normalize_mem_sphere line 1048
  123. def OAI.CKSSphericalHarmonics.normalizeSphere line 1053
  124. lemma OAI.CKSSphericalHarmonics.normalizeSphere_smooth line 1056
  125. def OAI.CKSSphericalHarmonics.radialExtension line 1066
  126. lemma OAI.CKSSphericalHarmonics.radialExtension_on_sphere line 1069
  127. theorem OAI.CKSSphericalHarmonics.radialExtension_smooth line 1077
  128. def OAI.CKSSphericalHarmonics.rotationGenerator line 1092
  129. lemma OAI.CKSSphericalHarmonics.rotationGenerator_apply line 1097
  130. lemma OAI.CKSSphericalHarmonics.rotationGenerator_smooth line 1102
  131. def OAI.CKSSphericalHarmonics.smoothRotation line 1105
  132. lemma OAI.CKSSphericalHarmonics.smoothRotation_smooth line 1108
  133. def OAI.CKSSphericalHarmonics.smoothRestriction line 1113
  134. lemma OAI.CKSSphericalHarmonics.planeRotation_hasDerivAt line 1116
  135. lemma OAI.CKSSphericalHarmonics.smoothRotation_orbit_derivative line 1142
  136. lemma OAI.CKSSphericalHarmonics.planeRotation_zero line 1152
  137. theorem OAI.CKSSphericalHarmonics.sphereIntegral_smoothRotation line 1160
  138. lemma OAI.CKSSphericalHarmonics.smoothRestriction_add line 1191
  139. lemma OAI.CKSSphericalHarmonics.smoothRestriction_mul line 1195
  140. lemma OAI.CKSSphericalHarmonics.smoothRotation_mul line 1199
  141. lemma OAI.CKSSphericalHarmonics.inner_toL2 line 1207
  142. theorem OAI.CKSSphericalHarmonics.smoothRotation_skew_adjoint line 1215
  143. def OAI.CKSSphericalHarmonics.polynomialExtension line 1235
  144. lemma OAI.CKSSphericalHarmonics.polynomialExtension_smooth line 1237
  145. lemma OAI.CKSSphericalHarmonics.polynomialExtension_on_sphere line 1249
  146. lemma OAI.CKSSphericalHarmonics.polynomialExtension_restriction line 1259
  147. lemma OAI.CKSSphericalHarmonics.smoothRotation_restriction_eq line 1264
  148. def OAI.CKSSphericalHarmonics.smoothCasimir line 1281
  149. lemma OAI.CKSSphericalHarmonics.smoothCasimir_smooth line 1286
  150. lemma OAI.CKSSphericalHarmonics.smoothRestriction_casimir line 1292
  151. lemma OAI.CKSSphericalHarmonics.smoothCasimir_restriction_eq line 1298
  152. lemma OAI.CKSSphericalHarmonics.smoothRotation_square_symmetric line 1307
  153. lemma OAI.CKSSphericalHarmonics.smoothCasimir_symmetric line 1318
  154. lemma OAI.CKSSphericalHarmonics.smooth_harmonic_pairing line 1328
  155. lemma OAI.CKSSphericalHarmonics.harmonicProjection_smoothCasimir line 1338
  156. def OAI.CKSSphericalHarmonics.smoothCasimirIterate line 1355
  157. lemma OAI.CKSSphericalHarmonics.smoothCasimirIterate_smooth line 1359
  158. lemma OAI.CKSSphericalHarmonics.harmonicProjection_smoothCasimirIterate line 1365
  159. theorem OAI.CKSSphericalHarmonics.harmonicProjection_rapid_L2 line 1377
  160. def OAI.CKSSphericalHarmonics.harmonicCoefficientPolynomial line 1387
  161. lemma OAI.CKSSphericalHarmonics.harmonicCoefficientPolynomial_spec line 1390
  162. lemma OAI.CKSSphericalHarmonics.harmonicCoefficientPolynomial_restriction line 1396
  163. def OAI.CKSSphericalHarmonics.rotatedHarmonicCoefficient line 1401
  164. lemma OAI.CKSSphericalHarmonics.rotatedHarmonicCoefficient_nil line 1404
  165. lemma OAI.CKSSphericalHarmonics.rotatedHarmonicCoefficient_bound line 1408
  166. lemma OAI.CKSSphericalHarmonics.eigenvalue_ge_degree line 1416
  167. lemma OAI.CKSSphericalHarmonics.rotatedHarmonicCoefficient_pseries_bound line 1421
  168. theorem OAI.CKSSphericalHarmonics.rotatedHarmonicCoefficient_rapid line 1455
  169. theorem OAI.CKSSphericalHarmonics.smoothSphere_actual_projections_rapid line 1471
  170. lemma OAI.CKSSphericalHarmonics.radialExtension_pos_smul line 1478
  171. lemma OAI.CKSSphericalHarmonics.radialExtension_isometry line 1490
  172. lemma OAI.CKSSphericalHarmonics.polynomial_sphere_smooth line 1498
  173. lemma OAI.CKSSphericalHarmonics.radialExtension_fderiv_self line 1504
  174. lemma OAI.CKSSphericalHarmonics.smoothRotation_radial_polynomial line 1518
  175. lemma OAI.CKSSphericalHarmonics.rotationGenerator_decomposition line 1544
  176. lemma OAI.CKSSphericalHarmonics.radial_polynomial_fderiv line 1552
  177. def OAI.CKSSpectralHeat.eigenvalue line 1578
  178. lemma OAI.CKSSpectralHeat.eigenvalue_ge_six line 1580
  179. lemma OAI.CKSSpectralHeat.eigenvalue_pos line 1584
  180. def OAI.CKSSpectralHeat.kernel line 1586
  181. lemma OAI.CKSSpectralHeat.kernel_smooth line 1588
  182. lemma OAI.CKSSpectralHeat.kernel_nonneg_time line 1590
  183. lemma OAI.CKSSpectralHeat.kernel_zero line 1593
  184. lemma OAI.CKSSpectralHeat.kernel_derivative_bounded line 1596
  185. lemma OAI.CKSSpectralHeat.kernel_deriv_nonneg_time line 1624
  186. def OAI.CKSSpectralHeat.Rapid line 1639
  187. def OAI.CKSSpectralHeat.term line 1642
  188. def OAI.CKSSpectralHeat.heat line 1645
  189. lemma OAI.CKSSpectralHeat.term_smooth line 1648
  190. lemma OAI.CKSSpectralHeat.term_deriv line 1653
  191. lemma OAI.CKSSpectralHeat.heat_majorant line 1664
  192. theorem OAI.CKSSpectralHeat.heat_smooth line 1680
  193. lemma OAI.CKSSpectralHeat.term_deriv_nonneg_time line 1684
  194. lemma OAI.CKSSpectralHeat.heat_eq_series line 1693
  195. lemma OAI.CKSSpectralHeat.heat_initial line 1701
  196. lemma OAI.CKSSpectralHeat.heat_deriv line 1705
  197. lemma OAI.CKSSpectralHeat.heat_deriv_nonneg_time line 1714
  198. lemma OAI.CKSSpectralHeat.term_decay line 1723
  199. theorem OAI.CKSSpectralHeat.heat_decay line 1738
  200. lemma OAI.CKSSpectralHeat.term_deriv_summable line 1752
  201. lemma OAI.CKSSpectralHeat.term_summable line 1759
  202. def OAI.CKSSpectralHeat.generator line 1763
  203. lemma OAI.CKSSpectralHeat.generator_rapid line 1766
  204. theorem OAI.CKSSpectralHeat.spectral_heat_equation line 1771
  205. def OAI.CKSSpectralHeat.inverseCoeff line 1781
  206. lemma OAI.CKSSpectralHeat.inverse_denominator_bound line 1784
  207. lemma OAI.CKSSpectralHeat.inverseCoeff_rapid line 1793
  208. theorem OAI.CKSSpectralHeat.heat_and_potential line 1807
  209. lemma OAI.CKSSpectralHeat.heat_map line 1832