OAI/Probability/InvariantIsing/Cavity/CavityQuadraticStepWeight.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.cavityQuadraticStepWeight line 13
2. lemma OAI.InvariantIsing.measurable_cavityQuadraticStepWeight line 20
3. lemma OAI.InvariantIsing.cavityQuadraticStepWeight_pos line 26
4. lemma OAI.InvariantIsing.cavityQuadraticStepWeight_eq_normalized line 31
5. theorem OAI.InvariantIsing.cavity_quadratic_step_weight_innovation_law line 61

   Source documentation

   The concrete backward polynomial weight supplies the normalized innovation law required at every ancestor in cavityInnovationTree_law.

   theorem cavity_quadratic_step_weight_innovation_law {d : ℕ}
       (K P C S : Matrix (Fin d) (Fin d) ℝ)
       (hK : K.transpose = K) (hC : C.transpose = C) (hS : S.PosSemidef)
       (ζ : ℝ) (hζ : 0 < ζ)
       (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).withDensity
         (fun z => ENNReal.ofReal (cavityQuadraticStepWeight K P C ζ (u, z) ^ ζ))).map
         (fun z => Matrix.toEuclideanCLM (𝕜 := ℝ) (1 - C * K)⁻¹ (u + z) -
   …

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