OAI/Probability/InvariantIsing/Gaussian/GaussianPatternSingularVariance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Dimension-free Gaussian variance for the physical rectangular operator norm.

  1. lemma OAI.InvariantIsing.finiteGaussian_lipschitz_variance line 13
  2. theorem OAI.InvariantIsing.gaussianPatternSingularMax_variance line 24
  3. theorem OAI.InvariantIsing.gaussianPatternSingularMin_variance line 30