OAI/Probability/InvariantIsing/Cavity/CavityGaussianRows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Gaussian rows used to generate the finite fresh frames. Their empirical Gram matrices converge almost surely to the identity at fixed frame width.

  1. def OAI.InvariantIsing.cavityGaussianRow line 16
  2. instance OAI.InvariantIsing.(instance at line 19) line 19
  3. def OAI.InvariantIsing.cavityGaussianRows line 22
  4. instance OAI.InvariantIsing.(instance at line 25) line 25
  5. lemma OAI.InvariantIsing.cavityGaussianRow_eval_law line 28
  6. lemma OAI.InvariantIsing.cavityGaussianRow_product_integrable line 32
  7. lemma OAI.InvariantIsing.cavityGaussianRow_product_integral line 40
  8. lemma OAI.InvariantIsing.cavityGaussianRows_eval_law line 59
  9. theorem OAI.InvariantIsing.cavityGaussianRows_gram_tendsto line 65

    Source documentation

    The fixed-width Gaussian Gram matrix tends to the identity.

    theorem cavityGaussianRows_gram_tendsto (q : ℕ) :
    ∀ᵐ x ∂cavityGaussianRows q,
      Tendsto (fun n i j => (∑ k ∈ Finset.range n, x k i * x k j) / (n : ℝ))
        atTop (𝓝 (1 : Matrix (Fin q) (Fin q) ℝ)) := by
…

    Mentions: OAI.InvariantIsing.cavityGaussianRows