OAI/Probability/InvariantIsing/Gaussian/GaussianPatternPressureLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian-pattern pressure limit from Haar concentration, cascade identities, Marchenko–Pastur convergence, and spectral edge estimates.

  1. def OAI.InvariantIsing.gaussianPatternLimit line 15

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:248 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.gaussianPatternLimit@path.

  2. theorem OAI.InvariantIsing.gaussianPattern_pressure_uniformIntegrable line 20
  3. theorem OAI.InvariantIsing.gaussianPattern_pressure_limit line 48