OAI/Probability/InvariantIsing/Cavity/CavitySphereMoments.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform even moments of Haar projections. Gaussian angular averaging gives a bound with the dimension in the denominator.

  1. theorem OAI.InvariantIsing.cavity_gaussian_angular_moment line 14
  2. theorem OAI.InvariantIsing.cavity_sphere_even_moment_bound line 55