OAI/Probability/InvariantIsing/Haar/HaarKernelMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative concentration of the positive polynomial kernels near the identity.

  1. lemma OAI.InvariantIsing.haarKernelMass_lower line 11
  2. lemma OAI.InvariantIsing.haarKernel_superlevel_pos line 28
  3. theorem OAI.InvariantIsing.haarKernelMass_ratio_tendsto_zero line 36