OAI/Probability/InvariantIsing/Cavity/CavityPrecisionTiltLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Identification of the full Gaussian law under a quadratic tilt. The proof uses the already computed Laplace transforms, so it does not require a density with respect to Lebesgue measure.

  1. lemma OAI.InvariantIsing.cavity_charFun_projection line 16
  2. lemma OAI.InvariantIsing.cavity_law_eq_of_projection_mgf line 25
  3. theorem OAI.InvariantIsing.cavity_precision_tilt_law line 51

    Source documentation

    The normalized quadratic tilt of a standard Gaussian has the full Gaussian law with mean Q⁻¹l and covariance Q⁻¹.

    theorem cavity_precision_tilt_law {d : ℕ}
    (Q : Matrix (Fin d) (Fin d) ℝ) (hQ : Q.PosDef) (l : EuclideanSpace ℝ (Fin d)) :
    (stdGaussian (EuclideanSpace ℝ (Fin d))).tilted (cavityPrecisionPotential Q l) =
      multivariateGaussian (Matrix.toEuclideanCLM (𝕜 := ℝ) Q⁻¹ l) Q⁻¹ := by
…

    Mentions: OAI.InvariantIsing.cavityPrecisionPotential