OAI/Probability/InvariantIsing/Cavity/CavityFrameLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The correction used to orthonormalize a fixed number of Gaussian columns converges to the identity.

  1. lemma OAI.InvariantIsing.cavity_gram_sqrt_tendsto line 14
  2. lemma OAI.InvariantIsing.cavity_gram_correction_tendsto line 26
  3. theorem OAI.InvariantIsing.cavityGaussian_correction_tendsto line 39
  4. theorem OAI.InvariantIsing.cavityGaussian_normalized_gram_eventually line 47