OAI/Probability/InvariantIsing/Cavity/CavityGaussianRadialMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Dimension-explicit Gaussian radial moments used to bound moments of uniform spherical projections.

  1. def OAI.InvariantIsing.cavityGaussianAbsMoment line 14
  2. lemma OAI.InvariantIsing.cavityGaussianAbsMoment_nonneg line 17
  3. lemma OAI.InvariantIsing.cavityGaussianAbsMoment_two line 20
  4. lemma OAI.InvariantIsing.cavity_gaussian_norm_pow_integrable line 26
  5. lemma OAI.InvariantIsing.cavity_gaussian_inner_abs_moment line 31
  6. lemma OAI.InvariantIsing.cavity_gaussian_norm_sq_integral line 51
  7. lemma OAI.InvariantIsing.cavity_gaussian_radial_moment_lower line 67