OAI/Probability/InvariantIsing/Gaussian/GaussianGramUniformIntegrability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The Davidson--Szarek uniform-integrability consequence for the physical Gram spectrum.

  1. lemma OAI.InvariantIsing.uniformIntegrable_nat_mul_real line 11
  2. theorem OAI.InvariantIsing.gaussianPattern_spectralRadius_uniformIntegrable line 22