OAI/MathematicalPhysics/CriticalSK/SphereGeometry.lean

GitHub source file

156 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.orthogonal_entry_bound line 48
  2. instance OAI.CriticalSK.orthogonalGroup_compactSpace line 60
  3. instance OAI.CriticalSK.orthogonalGroup_measurableSpace line 73
  4. instance OAI.CriticalSK.orthogonalGroup_borelSpace line 76
  5. def OAI.CriticalSK.orthogonalHaar line 78
  6. instance OAI.CriticalSK.orthogonalHaar_probability line 82
  7. instance OAI.CriticalSK.orthogonalHaar_leftInvariant line 86
  8. instance OAI.CriticalSK.orthogonalHaar_haar line 90
  9. instance OAI.CriticalSK.orthogonalHaar_rightInvariant line 94
  10. lemma OAI.CriticalSK.euclideanMatrix_mul_apply line 106
  11. lemma OAI.CriticalSK.euclideanMatrix_one_apply line 111
  12. lemma OAI.CriticalSK.orthogonal_inner_map line 115
  13. def OAI.CriticalSK.orthogonalIsometry line 123
  14. lemma OAI.CriticalSK.orthogonalIsometry_apply line 137
  15. lemma OAI.CriticalSK.orthogonalIsometry_mul line 140
  16. lemma OAI.CriticalSK.orthogonalIsometry_continuous line 144
  17. lemma OAI.CriticalSK.orthogonalIsometry_fixed_continuous line 158
  18. def OAI.CriticalSK.matrixOfIsometry line 171
  19. lemma OAI.CriticalSK.orthogonalIsometry_matrixOfIsometry line 175
  20. lemma OAI.CriticalSK.orthogonal_transitive line 183
  21. def OAI.CriticalSK.sphereMap line 196
  22. lemma OAI.CriticalSK.sphereMap_continuous line 199
  23. lemma OAI.CriticalSK.sphereMap_symm line 202
  24. lemma OAI.CriticalSK.sphereMap_cone_preimage line 207
  25. lemma OAI.CriticalSK.sphereMap_preserving line 224
  26. abbrev OAI.CriticalSK.unitSphere line 242
  27. def OAI.CriticalSK.orthogonalSphere line 244
  28. lemma OAI.CriticalSK.orthogonalSphere_continuous line 247
  29. lemma OAI.CriticalSK.orthogonalSphere_mul line 252
  30. lemma OAI.CriticalSK.orthogonalSphere_transitive line 257
  31. lemma OAI.CriticalSK.orthogonalSphere_integral line 263
  32. lemma OAI.CriticalSK.orthogonal_orbit_integral_eq line 272
  33. def OAI.CriticalSK.sphereArea line 282
  34. def OAI.CriticalSK.sphereAverage line 284
  35. lemma OAI.CriticalSK.sphereArea_pos line 288
  36. lemma OAI.CriticalSK.orthogonal_first_moment line 292
  37. def OAI.CriticalSK.sphereUniform line 323
  38. instance OAI.CriticalSK.sphereUniform_probability line 327
  39. lemma OAI.CriticalSK.sphereUniform_integral line 334
  40. lemma OAI.CriticalSK.orthogonal_sphere_preserving line 339
  41. lemma OAI.CriticalSK.orthogonal_pair_transitive line 358
  42. lemma OAI.CriticalSK.orthogonal_pair_integral_eq line 380
  43. lemma OAI.CriticalSK.orthogonal_pair_swap line 391
  44. def OAI.CriticalSK.diagonalEnergy line 397
  45. lemma OAI.CriticalSK.diagonalEnergy_continuous line 400
  46. lemma OAI.CriticalSK.orthogonalHaar_integrable line 405
  47. def OAI.CriticalSK.pairIntegrand line 409
  48. def OAI.CriticalSK.pairMoment line 414
  49. lemma OAI.CriticalSK.pairIntegrand_continuous line 417
  50. lemma OAI.CriticalSK.pairMoment_nonneg line 423
  51. lemma OAI.CriticalSK.pairMoment_even line 426
  52. lemma OAI.CriticalSK.exp_pair_cosh line 436
  53. lemma OAI.CriticalSK.pairMoment_cosh line 442
  54. lemma OAI.CriticalSK.pairMoment_mono_abs line 466
  55. def OAI.CriticalSK.spherePartition line 493
  56. lemma OAI.CriticalSK.sphere_energy_continuous line 497
  57. lemma OAI.CriticalSK.orthogonal_scaled_partition line 504
  58. lemma OAI.CriticalSK.orthogonal_radial_partition line 516
  59. lemma OAI.CriticalSK.cubeVector_norm line 536
  60. def OAI.CriticalSK.rotatedCubePartition line 543
  61. lemma OAI.CriticalSK.rotatedCubePartition_first_moment line 548
  62. def OAI.CriticalSK.overlapPlus line 565
  63. def OAI.CriticalSK.overlapMinus line 568
  64. lemma OAI.CriticalSK.overlapPair_gram line 572
  65. lemma OAI.CriticalSK.diagonalEnergy_overlap line 601
  66. lemma OAI.CriticalSK.pair_energy_orbit line 620
  67. lemma OAI.CriticalSK.pairMoment_continuous line 648
  68. lemma OAI.CriticalSK.sphereUniform_rotation_preserving line 670
  69. lemma OAI.CriticalSK.orthogonalSphere_injective line 675
  70. lemma OAI.CriticalSK.orthogonalSphere_fixed_continuous line 682
  71. lemma OAI.CriticalSK.spherePair_rotation_integral line 685
  72. lemma OAI.CriticalSK.continuous_pair_first line 699
  73. lemma OAI.CriticalSK.continuous_pair_second line 705
  74. lemma OAI.CriticalSK.spherePair_first_continuous line 711
  75. lemma OAI.CriticalSK.spherePair_second_continuous line 717
  76. lemma OAI.CriticalSK.spherePair_action_continuous line 723
  77. lemma OAI.CriticalSK.spherePair_haar_average line 728
  78. lemma OAI.CriticalSK.sphere_inner_abs_le_one line 742
  79. def OAI.CriticalSK.spherePairEnergy line 747
  80. lemma OAI.CriticalSK.spherePairEnergy_factor line 751
  81. lemma OAI.CriticalSK.spherePairEnergy_continuous line 761
  82. lemma OAI.CriticalSK.spherePairEnergy_integral line 770
  83. lemma OAI.CriticalSK.spectrum_pair_second_moment line 779
  84. def OAI.CriticalSK.sphereOverlapLaw line 801
  85. lemma OAI.CriticalSK.sphereOverlap_second_moment line 805
  86. def OAI.CriticalSK.spinProduct line 818
  87. lemma OAI.CriticalSK.spinValue_beq line 820
  88. lemma OAI.CriticalSK.spinProduct_involution line 823
  89. def OAI.CriticalSK.spinProductEquiv line 829
  90. def OAI.CriticalSK.signMean line 832
  91. lemma OAI.CriticalSK.cubeOverlap_signMean line 834
  92. lemma OAI.CriticalSK.cubeOverlap_abs_le_one line 840
  93. lemma OAI.CriticalSK.cubeOverlap_gram line 849
  94. lemma OAI.CriticalSK.cubeOverlap_sum line 854
  95. lemma OAI.CriticalSK.cubeOverlap_average line 859
  96. def OAI.CriticalSK.spinFinsetEquiv line 867
  97. lemma OAI.CriticalSK.signMean_finset line 877
  98. lemma OAI.CriticalSK.finset_card_sum line 889
  99. lemma OAI.CriticalSK.cubeOverlap_binomial_sum line 899
  100. lemma OAI.CriticalSK.rotatedCubePartition_continuous line 910
  101. lemma OAI.CriticalSK.rotatedCubePartition_square line 918
  102. lemma OAI.CriticalSK.cube_pair_energy_continuous line 935
  103. lemma OAI.CriticalSK.rotatedCubePartition_second_moment line 943
  104. lemma OAI.CriticalSK.integral_polar line 970
  105. lemma OAI.CriticalSK.radial_map_preserving line 983
  106. lemma OAI.CriticalSK.lintegral_polar line 993
  107. def OAI.CriticalSK.radialGaussian line 1003
  108. lemma OAI.CriticalSK.radialGaussian_finite line 1006
  109. lemma OAI.CriticalSK.radialGaussian_pos line 1014
  110. lemma OAI.CriticalSK.lintegral_scale_pos line 1024
  111. lemma OAI.CriticalSK.lintegral_scale_pos_Ioi line 1033
  112. lemma OAI.CriticalSK.radialGaussian_scaled line 1047
  113. lemma OAI.CriticalSK.radialGaussian_polar line 1066
  114. lemma OAI.CriticalSK.volumeIoiPow_lintegral line 1094
  115. lemma OAI.CriticalSK.lintegral_radial_norm line 1106
  116. def OAI.CriticalSK.sphereRatio line 1122
  117. def OAI.CriticalSK.sphereRatioInv line 1124
  118. lemma OAI.CriticalSK.sphereRatio_den_pos line 1126
  119. lemma OAI.CriticalSK.sphereRatio_sq line 1128
  120. lemma OAI.CriticalSK.one_sub_sphereRatio_sq line 1131
  121. lemma OAI.CriticalSK.sphereRatio_mem line 1136
  122. lemma OAI.CriticalSK.sphereRatioInv_den_pos line 1140
  123. lemma OAI.CriticalSK.one_add_sphereRatioInv_sq line 1143
  124. lemma OAI.CriticalSK.sphereRatio_left_inverse line 1149
  125. lemma OAI.CriticalSK.sphereRatio_right_inverse line 1156
  126. lemma OAI.CriticalSK.sphereRatio_injective line 1164
  127. lemma OAI.CriticalSK.sphereRatioInv_injOn line 1167
  128. lemma OAI.CriticalSK.sphereRatioInv_image line 1172
  129. lemma OAI.CriticalSK.sphereRatioInv_hasDerivAt line 1177
  130. lemma OAI.CriticalSK.sphereRatioInv_continuousOn line 1191
  131. def OAI.CriticalSK.sphereOverlapShape line 1194
  132. lemma OAI.CriticalSK.sphereRatioInv_jacobian_shape line 1196
  133. lemma OAI.CriticalSK.sphereRatio_integral line 1207
  134. def OAI.CriticalSK.cylinderKernel line 1221
  135. lemma OAI.CriticalSK.cylinderKernel_measurable line 1224
  136. lemma OAI.CriticalSK.scaled_ratio line 1229
  137. lemma OAI.CriticalSK.cylinderKernel_scaled line 1235
  138. lemma OAI.CriticalSK.cylinder_scalar_scale line 1244
  139. lemma OAI.CriticalSK.cylinder_radius_integral line 1252
  140. def OAI.CriticalSK.euclidSplit line 1286
  141. lemma OAI.CriticalSK.euclidSplit_preserving line 1289
  142. lemma OAI.CriticalSK.euclidSplit_norm_sq line 1297
  143. lemma OAI.CriticalSK.euclidSplit_norm line 1302
  144. lemma OAI.CriticalSK.euclidSplit_integral line 1306
  145. lemma OAI.CriticalSK.gaussian_cylinder_volume line 1321
  146. lemma OAI.CriticalSK.gaussian_coordinate_polar line 1349
  147. lemma OAI.CriticalSK.sphere_coordinate_lintegral line 1366
  148. def OAI.CriticalSK.overlapShapeMeasure line 1376
  149. def OAI.CriticalSK.normalizedOverlapShape line 1379
  150. lemma OAI.CriticalSK.overlapShapeMeasure_lintegral line 1382
  151. lemma OAI.CriticalSK.overlapShapeMeasure_univ line 1388
  152. lemma OAI.CriticalSK.sphereUniform_coordinate_lintegral line 1393
  153. def OAI.CriticalSK.firstUnit line 1409
  154. lemma OAI.CriticalSK.sphere_inner_coordinate_lintegral line 1412
  155. lemma OAI.CriticalSK.sphereOverlapLaw_lintegral line 1427
  156. lemma OAI.CriticalSK.sphereOverlapLaw_density line 1435