OAI/Probability/InvariantIsing/Cavity/CavityScalarFieldLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A scalar covariance compression of the transformed Gaussian cavity field is exactly a product of independent one-site Gaussian laws.

  1. theorem OAI.InvariantIsing.cavity_rectangularGaussian_image line 16
  2. theorem OAI.InvariantIsing.cavity_scalarGaussian_ofLp_law line 43
  3. theorem OAI.InvariantIsing.cavity_scalar_projected_field_law line 84

    Source documentation

    Once a transformed covariance is scalar, the actual projected field has the product law used by the one-site recursion.

    theorem cavity_scalar_projected_field_law {d n : ℕ}
    (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosSemidef)
    (L : Matrix (Fin d) (Fin n) ℝ) (v : ℝ≥0)
    (hcov : L.transpose * S * L = (v : ℝ) • 1) :
    MeasurePreserving (fun z : EuclideanSpace ℝ (Fin d) =>
      WithLp.ofLp (L.transpose.toEuclideanLin z))
      (multivariateGaussian 0 S) (vectorGaussianLaw n v : Measure (Fin n → ℝ)) := by
…

    Mentions: OAI.InvariantIsing.vectorGaussianLaw