OAI/MathematicalPhysics/CriticalSK/PartitionBounds.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.log_le_square_half line 58
  2. lemma OAI.CriticalSK.gaussian_radial_shape_bound line 64
  3. lemma OAI.CriticalSK.diagonalGaussian_normSq_integrable line 93
  4. lemma OAI.CriticalSK.diagonalGaussian_normSq_mean line 101
  5. lemma OAI.CriticalSK.diagonalGaussian_singleton_zero line 106
  6. lemma OAI.CriticalSK.diagonalGaussian_standard_shell_half line 111
  7. lemma OAI.CriticalSK.diagonalSquareDensity_standard_formula line 148
  8. lemma OAI.CriticalSK.standard_radial_density_upper line 157
  9. lemma OAI.CriticalSK.diagonalSquareDensity_standard_lower line 171
  10. def OAI.CriticalSK.spectralTop line 202
  11. lemma OAI.CriticalSK.le_spectralTop line 204
  12. lemma OAI.CriticalSK.spectralTop_attained line 207
  13. def OAI.CriticalSK.spectralStieltjes line 211
  14. def OAI.CriticalSK.spectralStieltjesSlope line 214
  15. lemma OAI.CriticalSK.cardinal_pos_real line 217
  16. lemma OAI.CriticalSK.spectralStieltjes_pos line 219
  17. lemma OAI.CriticalSK.spectralStieltjes_strictAnti line 225
  18. lemma OAI.CriticalSK.spectralStieltjes_hasStrictDerivAt line 234
  19. lemma OAI.CriticalSK.spectralStieltjesSlope_neg line 243
  20. lemma OAI.CriticalSK.spectralStieltjes_continuous line 249
  21. lemma OAI.CriticalSK.spectralStieltjes_exists line 252
  22. def OAI.CriticalSK.saddleRadius line 292
  23. lemma OAI.CriticalSK.saddleRadius_spec line 295
  24. lemma OAI.CriticalSK.saddleRadius_unique line 299
  25. lemma OAI.CriticalSK.saddleRadius_hasStrictDerivAt line 305
  26. def OAI.CriticalSK.saddleObjective line 315
  27. def OAI.CriticalSK.sphericalVariational line 318
  28. def OAI.CriticalSK.saddleZ line 321
  29. lemma OAI.CriticalSK.saddleZ_pos_gap line 324
  30. lemma OAI.CriticalSK.saddleZ_gap_pos line 331
  31. lemma OAI.CriticalSK.saddleZ_reciprocal_sum line 336
  32. lemma OAI.CriticalSK.saddleObjective_min line 349
  33. lemma OAI.CriticalSK.sphericalVariational_eq line 372
  34. lemma OAI.CriticalSK.sphericalVariational_zero line 380
  35. lemma OAI.CriticalSK.sphericalVariational_radius_expr line 384
  36. lemma OAI.CriticalSK.sphericalVariational_hasDerivAt line 397
  37. lemma OAI.CriticalSK.saddleZ_weighted_identity line 427
  38. lemma OAI.CriticalSK.sphericalVariational_slope_bound line 438
  39. lemma OAI.CriticalSK.sphericalVariational_abs_le line 461
  40. lemma OAI.CriticalSK.sphericalVariational_continuousOn line 497
  41. lemma OAI.CriticalSK.gaussianPiPrefactor_log line 523
  42. lemma OAI.CriticalSK.gaussianPiPrefactor_log_ratio line 535
  43. lemma OAI.CriticalSK.spherical_gaussian_identity line 547
  44. lemma OAI.CriticalSK.saddleZ_le_bound line 577
  45. def OAI.CriticalSK.saddleVariance line 587
  46. lemma OAI.CriticalSK.saddleVariance_coe line 590
  47. lemma OAI.CriticalSK.saddleVariance_pos line 594
  48. lemma OAI.CriticalSK.saddleVariance_lower line 599
  49. lemma OAI.CriticalSK.gaussianPairPrefactor_bound line 608
  50. lemma OAI.CriticalSK.spherePartition_upper line 625
  51. lemma OAI.CriticalSK.diagonalSquareDensity_standard_upper line 660
  52. lemma OAI.CriticalSK.spherePartition_fixed_lower line 671
  53. lemma OAI.CriticalSK.gaussianPairPrefactor_lower line 707
  54. def OAI.CriticalSK.fixedBulkDeficit line 723
  55. lemma OAI.CriticalSK.fixedBulkDeficit_bounds line 726
  56. lemma OAI.CriticalSK.spectralGood_sphere_moment line 738
  57. lemma OAI.CriticalSK.spectralGood_sphere_overlap line 761
  58. lemma OAI.CriticalSK.spectralGood_sphere_partition_lower line 775