OAI/Probability/InvariantIsing/Cavity/CavityGram.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Eventual nondegeneracy of the Gaussian Gram matrix used to construct fresh orthonormal directions.

  1. def OAI.InvariantIsing.cavityEmpiricalGram line 14
  2. lemma OAI.InvariantIsing.cavityEmpiricalGram_posSemidef line 18
  3. lemma OAI.InvariantIsing.cavity_posDef_of_posSemidef_det_ne_zero line 31
  4. lemma OAI.InvariantIsing.cavityEmpiricalGram_tendsto line 42
  5. theorem OAI.InvariantIsing.cavityEmpiricalGram_eventually_posDef line 49

    Source documentation

    Almost every Gaussian row sequence yields nondegenerate Gram matrices at all sufficiently large sample sizes.

    theorem cavityEmpiricalGram_eventually_posDef (q : ℕ) :
    ∀ᵐ x ∂cavityGaussianRows q, ∀ᶠ n in atTop, (cavityEmpiricalGram x n).PosDef := by
…

    Mentions: OAI.InvariantIsing.cavityGaussianRows, OAI.InvariantIsing.cavityEmpiricalGram