OAI/MathematicalPhysics/CriticalSK/OverlapMoments.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.sphereInner_rotation line 72
  2. lemma OAI.CriticalSK.spherePairEnergy_haar line 77
  3. lemma OAI.CriticalSK.sphereOverlap_weighted_pair line 93
  4. lemma OAI.CriticalSK.sphereTilted_uniform_integral line 114
  5. lemma OAI.CriticalSK.sphereTilted_pair_integral line 123
  6. def OAI.CriticalSK.coordinateReflection line 147
  7. lemma OAI.CriticalSK.coordinateReflection_apply line 151
  8. lemma OAI.CriticalSK.coordinateReflection_energy line 157
  9. lemma OAI.CriticalSK.sphereMap_measurableEmbedding line 166
  10. lemma OAI.CriticalSK.sphereTilted_coordinate_cross line 175
  11. lemma OAI.CriticalSK.gaussianPairPrefactor_antitone line 199
  12. lemma OAI.CriticalSK.gaussianSquareCoordinateDensity_upper_all line 214
  13. lemma OAI.CriticalSK.sphereTilted_coordinate_sq_upper_all line 242
  14. lemma OAI.CriticalSK.sphereTilted_continuous_integrable line 275
  15. lemma OAI.CriticalSK.sphereTilted_linear_square line 279
  16. lemma OAI.CriticalSK.sphereTilted_linear_square_le line 302
  17. lemma OAI.CriticalSK.sphereTilted_overlap_moment line 316
  18. lemma OAI.CriticalSK.sphereTilted_overlap_bound line 333
  19. lemma OAI.CriticalSK.sphereOverlap_weighted_tilted line 344
  20. lemma OAI.CriticalSK.sphereOverlap_square_moment line 356