OAI/Probability/InvariantIsing/Gaussian/MPMeasureSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The precise support and both endpoint clauses of the Gaussian MP input.

  1. lemma OAI.InvariantIsing.mp_continuous_support_bound line 11
  2. theorem OAI.InvariantIsing.marchenkoPastur_support_bound line 19
  3. theorem OAI.InvariantIsing.marchenkoPastur_right_mem line 40
  4. theorem OAI.InvariantIsing.marchenkoPastur_left_mem line 44