OAI/Probability/InvariantIsing/Gaussian/GaussianPatternOrbitLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Haar disintegration of the actual Gaussian-pattern pressure, proved from finite Gaussian invariance and pointwise spectral diagonalization.

  1. lemma OAI.InvariantIsing.continuous_gaussianPatternRotation line 12
  2. lemma OAI.InvariantIsing.gaussianPattern_orbit_kernel line 29
  3. theorem OAI.InvariantIsing.gaussianPattern_conditionalOrbit line 39
  4. theorem OAI.InvariantIsing.gaussianPattern_conditionalOrbit_hasLaw line 61