OAI/Probability/InvariantIsing/Cavity/CavityGramProbability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The nondegenerate Gaussian frames have probability tending to one. This also supplies the positive mass needed to condition the finite frame construction, without any assertion about zero sets of polynomials.

  1. lemma OAI.InvariantIsing.continuous_cavityEmpiricalGram line 15
  2. def OAI.InvariantIsing.cavityGoodGram line 24
  3. lemma OAI.InvariantIsing.measurableSet_cavityGoodGram line 27
  4. lemma OAI.InvariantIsing.cavityGoodGram_ae_eventually line 30
  5. theorem OAI.InvariantIsing.cavityGoodGram_probability_tendsto line 36
  6. lemma OAI.InvariantIsing.cavityGoodGram_eventually_positive line 58