OAI/Probability/InvariantIsing/Gaussian/GaussianPatternEigenvalueMeasurability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Measurability of the actual sorted Gaussian Gram spectrum, including repeated zero roots.

  1. lemma OAI.InvariantIsing.continuous_hermitian_eigenvaluesâ‚€ line 11
  2. lemma OAI.InvariantIsing.continuous_hermitian_eigenvalues line 19
  3. lemma OAI.InvariantIsing.continuous_gaussianPatternCoupling line 26
  4. theorem OAI.InvariantIsing.continuous_gaussianPatternEigenvalues line 31
  5. theorem OAI.InvariantIsing.measurable_gaussianPatternEigenvalues line 37