OAI/Probability/InvariantIsing/Cavity/CavityGaussianInnovation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The centered innovation of a retained quadratic Gaussian step.

  1. lemma OAI.InvariantIsing.cavity_shifted_gaussian_quadratic_tilt_law line 15
  2. theorem OAI.InvariantIsing.cavity_gaussian_step_innovation_law line 39

    Source documentation

    Under the retained quadratic weight, the rescaled increment has an ancestor-independent centered Gaussian law.

    theorem cavity_gaussian_step_innovation_law {d : ℕ}
    (K P C S : Matrix (Fin d) (Fin d) ℝ)
    (hK : K.transpose = K) (hC : C.transpose = C) (hS : S.PosSemidef)
    (ζ : ℝ) (hPdet : IsUnit (1 - P * K).det) (hCdet : IsUnit (1 - C * K).det)
    (hΔ : P - C = ζ • S)
    (hQ : (cavityFactorPrecision (ζ • cavityBackwardQuadratic K C)
      (CFC.sqrt S)).PosDef) (u : EuclideanSpace ℝ (Fin d)) :
    ((multivariateGaussian 0 S).tilted
      (fun z => ζ / 2 * ⟪u + z, Matrix.toEuclideanCLM (𝕜 := ℝ)
…

    Mentions: OAI.InvariantIsing.cavityFactorPrecision, OAI.InvariantIsing.cavityBackwardQuadratic