OAI/Probability/InvariantIsing/Cavity/CavityGaussianForestLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite restrictions of the independent Gaussian forest, and the literal sum of its marks along a labeled cavity leaf.

  1. lemma OAI.InvariantIsing.cavity_labeled_leaf_sum line 16
  2. theorem OAI.InvariantIsing.cavity_gaussian_finite_node_law line 26

    Source documentation

    A finite set of distinct nodes can be sampled from the full product law before taking any linear replica projections.

    theorem cavity_gaussian_finite_node_law {A J : Type*} [Fintype J] [DecidableEq J]
    {d r : ℕ} (e : J → A) (he : Function.Injective e)
    (S : A → 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 (e a) p.2 q.2) :
    (Measure.infinitePi (fun a => multivariateGaussian
      (0 : EuclideanSpace ℝ (Fin d)) (S a))).map
        (fun z => cavityGaussianNodeSum w (fun a => z (e a))) =
          multivariateGaussian 0 Q := by
…

    Mentions: OAI.InvariantIsing.cavityGaussianNodeSum