OAI/MathematicalPhysics/CriticalSK/SphereSaddle.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalSK.gaussianPiPDF line 69
  2. lemma OAI.CriticalSK.gaussianPiPDF_nonneg line 72
  3. lemma OAI.CriticalSK.gaussianPiPDF_integrable line 75
  4. lemma OAI.CriticalSK.gaussianPi_density line 78
  5. lemma OAI.CriticalSK.gaussianPiPDF_continuous line 101
  6. lemma OAI.CriticalSK.map_density_of_preserving line 105
  7. def OAI.CriticalSK.diagonalGaussian line 114
  8. lemma OAI.CriticalSK.density_toLp line 117
  9. lemma OAI.CriticalSK.diagonalGaussian_density line 126
  10. instance OAI.CriticalSK.diagonalGaussian_probability line 133
  11. lemma OAI.CriticalSK.euclideanGaussianPDF_continuous line 137
  12. lemma OAI.CriticalSK.euclideanGaussianPDF_integrable line 141
  13. lemma OAI.CriticalSK.integral_polar_iterated line 153
  14. lemma OAI.CriticalSK.angular_integral_continuous line 162
  15. lemma OAI.CriticalSK.integral_polar_real line 171
  16. def OAI.CriticalSK.normShell line 187
  17. lemma OAI.CriticalSK.normShell_measurable line 190
  18. lemma OAI.CriticalSK.normShell_radial line 195
  19. lemma OAI.CriticalSK.normShell_integral line 201
  20. def OAI.CriticalSK.radialDensity line 231
  21. lemma OAI.CriticalSK.radialDensity_continuous line 235
  22. lemma OAI.CriticalSK.normShell_density line 241
  23. lemma OAI.CriticalSK.normShell_density_real line 250
  24. lemma OAI.CriticalSK.normShell_density_limit line 259
  25. def OAI.CriticalSK.squareNormShell line 277
  26. lemma OAI.CriticalSK.squareNormShell_measurable line 280
  27. lemma OAI.CriticalSK.squareNormShell_eq line 285
  28. lemma OAI.CriticalSK.squareNormShell_density_limit line 296
  29. def OAI.CriticalSK.splitPair line 322
  30. lemma OAI.CriticalSK.splitPair_preserving line 325
  31. lemma OAI.CriticalSK.splitPair_square_sum line 335
  32. def OAI.CriticalSK.squareDisk line 343
  33. def OAI.CriticalSK.squareAnnulus line 345
  34. lemma OAI.CriticalSK.squareDisk_measurable line 348
  35. lemma OAI.CriticalSK.squareAnnulus_measurable line 351
  36. lemma OAI.CriticalSK.squareDisk_complex line 356
  37. lemma OAI.CriticalSK.volume_squareDisk line 365
  38. lemma OAI.CriticalSK.squareAnnulus_sdiff line 372
  39. lemma OAI.CriticalSK.volume_squareAnnulus line 377
  40. def OAI.CriticalSK.gaussianPairPrefactor line 391
  41. lemma OAI.CriticalSK.gaussianPairPrefactor_nonneg line 394
  42. lemma OAI.CriticalSK.gaussianPair_density line 398
  43. lemma OAI.CriticalSK.gaussianPair_density_upper line 408
  44. lemma OAI.CriticalSK.gaussianPair_density_lower line 416
  45. lemma OAI.CriticalSK.gaussianPair_apply line 435
  46. lemma OAI.CriticalSK.gaussianPair_annulus_upper line 445
  47. lemma OAI.CriticalSK.gaussianPair_annulus_lower line 459
  48. lemma OAI.CriticalSK.volume_squareAnnulus_le line 480
  49. lemma OAI.CriticalSK.gaussianPair_annulus_upper_all line 499
  50. def OAI.CriticalSK.sumSquareShell line 515
  51. lemma OAI.CriticalSK.sumSquareShell_measurable line 518
  52. lemma OAI.CriticalSK.sumSquareShell_apply line 523
  53. lemma OAI.CriticalSK.gaussianPair_bulk_upper line 534
  54. lemma OAI.CriticalSK.gaussianPair_bulk_lower line 545
  55. lemma OAI.CriticalSK.fourth_power_le_exp line 575
  56. lemma OAI.CriticalSK.gaussian_fourth_integrable line 580
  57. lemma OAI.CriticalSK.gaussian_fourth_bound line 586
  58. lemma OAI.CriticalSK.gaussian_as_scaled line 605
  59. lemma OAI.CriticalSK.gaussian_fourth_integrable_var line 613
  60. lemma OAI.CriticalSK.gaussian_fourth_bound_var line 619
  61. lemma OAI.CriticalSK.gaussian_square_memLp line 629
  62. lemma OAI.CriticalSK.gaussian_square_mean line 634
  63. lemma OAI.CriticalSK.gaussian_square_variance line 640
  64. def OAI.CriticalSK.piSquareSum line 649
  65. lemma OAI.CriticalSK.piSquareSum_memLp line 651
  66. lemma OAI.CriticalSK.piSquareSum_mean line 656
  67. lemma OAI.CriticalSK.piSquareSum_variance line 667
  68. lemma OAI.CriticalSK.piSquareSum_tail line 677
  69. lemma OAI.CriticalSK.piSquareSum_bulk_mass line 685
  70. lemma OAI.CriticalSK.diagonalGaussian_shell_split line 728
  71. lemma OAI.CriticalSK.diagonalGaussian_shell_upper line 743
  72. lemma OAI.CriticalSK.diagonalGaussian_shell_lower line 750
  73. def OAI.CriticalSK.diagonalSquareDensity line 771
  74. lemma OAI.CriticalSK.diagonalSquareDensity_limit line 775
  75. lemma OAI.CriticalSK.diagonalSquareDensity_upper line 783
  76. lemma OAI.CriticalSK.diagonalSquareDensity_lower line 796
  77. def OAI.CriticalSK.radialEval line 828
  78. lemma OAI.CriticalSK.radialEval_embedding line 830
  79. def OAI.CriticalSK.radialCone line 834
  80. lemma OAI.CriticalSK.radialCone_measurable line 836
  81. lemma OAI.CriticalSK.radialCone_mem line 839
  82. lemma OAI.CriticalSK.angular_indicator_integral line 844
  83. def OAI.CriticalSK.radialDensityOn line 856
  84. lemma OAI.CriticalSK.radialDensityOn_continuous line 859
  85. lemma OAI.CriticalSK.normShell_cone_density_real line 866
  86. lemma OAI.CriticalSK.squareNormShell_cone_density_limit line 886
  87. lemma OAI.CriticalSK.gaussianPair_bulk_restricted_upper line 914
  88. lemma OAI.CriticalSK.gaussian_density_upper line 940
  89. lemma OAI.CriticalSK.gaussian_smallBall_upper line 949
  90. lemma OAI.CriticalSK.diagonalGaussian_shell_restricted_upper line 971
  91. lemma OAI.CriticalSK.radialCone_coordinate_bound line 994
  92. lemma OAI.CriticalSK.diagonalGaussian_shell_cone_upper line 1010
  93. def OAI.CriticalSK.diagonalSquareDensityOn line 1041
  94. lemma OAI.CriticalSK.diagonalSquareDensityOn_limit line 1046
  95. lemma OAI.CriticalSK.diagonalSquareDensityOn_smallBall line 1056
  96. lemma OAI.CriticalSK.sphereAverage_one line 1085
  97. def OAI.CriticalSK.gaussianPiPrefactor line 1090
  98. lemma OAI.CriticalSK.gaussianPiPDF_exp line 1093
  99. lemma OAI.CriticalSK.gaussianPiPrefactor_pos line 1099
  100. lemma OAI.CriticalSK.unitSphere_sum_sq line 1107
  101. lemma OAI.CriticalSK.sphereGaussianPDF line 1112
  102. lemma OAI.CriticalSK.radialDensity_spherePartition line 1133
  103. lemma OAI.CriticalSK.spherePartition_zero line 1145
  104. lemma OAI.CriticalSK.spherePartition_pos line 1148
  105. lemma OAI.CriticalSK.radialDensity_standard line 1159
  106. lemma OAI.CriticalSK.radialDensity_standard_pos line 1167
  107. lemma OAI.CriticalSK.spherical_radial_ratio line 1173
  108. def OAI.CriticalSK.sphereTilted line 1197
  109. lemma OAI.CriticalSK.sphereWeight_integrable line 1204
  110. lemma OAI.CriticalSK.sphereWeight_integral_pos line 1211
  111. instance OAI.CriticalSK.sphereTilted_probability line 1218
  112. lemma OAI.CriticalSK.sphereTilted_apply_real line 1227
  113. lemma OAI.CriticalSK.sphereTilted_density_ratio line 1241
  114. lemma OAI.CriticalSK.gaussianPairPrefactor_pos line 1263
  115. lemma OAI.CriticalSK.sphereTilted_smallBall line 1270
  116. lemma OAI.CriticalSK.gaussian_square_pdf_le_double line 1306
  117. lemma OAI.CriticalSK.gaussianPiPDF_square_le_double line 1350
  118. lemma OAI.CriticalSK.sphereTilted_integral line 1374
  119. lemma OAI.CriticalSK.sphereTilted_gaussian_integral line 1387
  120. lemma OAI.CriticalSK.angular_continuous_integrable line 1403
  121. def OAI.CriticalSK.gaussianSquareCoordinateDensity line 1410
  122. lemma OAI.CriticalSK.sphereTilted_coordinate_sq line 1414
  123. lemma OAI.CriticalSK.gaussianSquareCoordinateDensity_le_double line 1427
  124. lemma OAI.CriticalSK.gaussianSquareCoordinateDensity_upper line 1455
  125. lemma OAI.CriticalSK.sphereTilted_coordinate_sq_upper line 1474