OAI/Probability/InvariantIsing/Cavity/CavityGaussianNodeLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite projections of independent Gaussian nodes. Repeated use of a node retains its covariance, as required by the shared prefixes of replicas.

  1. lemma OAI.InvariantIsing.cavity_gaussian_node_coordinate_memLp line 17
  2. lemma OAI.InvariantIsing.cavity_gaussian_node_coordinate_covariance line 26
  3. def OAI.InvariantIsing.cavityGaussianNodeSum line 51
  4. lemma OAI.InvariantIsing.cavity_gaussian_node_sum_hasGaussianLaw line 56
  5. lemma OAI.InvariantIsing.cavity_gaussian_node_sum_covariance line 78
  6. lemma OAI.InvariantIsing.cavity_gaussian_node_coordinate_mean line 102
  7. lemma OAI.InvariantIsing.cavity_gaussian_node_sum_mean line 118
  8. theorem OAI.InvariantIsing.cavity_gaussian_node_sum_law line 139

    Source documentation

    The covariance of a finite collection of linear node sums determines its full joint law, including singular covariances.

    theorem cavity_gaussian_node_sum_law {J : Type*} [Fintype J] [DecidableEq J]
    (S : J → Matrix (Fin d) (Fin d) ℝ) (hS : ∀ a, (S a).PosSemidef)
    (w : Fin r → J → ℝ)
    (Q : Matrix (Fin r × Fin d) (Fin r × Fin d) ℝ) (hQ : Q.PosSemidef)
    (hcov : ∀ p q, Q p q = ∑ a, w p.1 a * w q.1 a * S a p.2 q.2) :
    (Measure.pi (fun a => multivariateGaussian 0 (S a))).map
      (cavityGaussianNodeSum w) = multivariateGaussian 0 Q := by
…

    Mentions: OAI.InvariantIsing.cavityGaussianNodeSum