CavityRetainedWeight.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Normalized fractional weights for the quadratic retained marks.

lemma OAI.InvariantIsing.cavity_retained_weight_density line 13

theorem OAI.InvariantIsing.cavity_retained_gaussian_innovation_law line 28

Source documentation

The fractional density used in the retained tree is exactly the normalized quadratic tilt, with no ordinary terminal exponential moment required.

theorem cavity_retained_gaussian_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)) :
    let f := fun z : EuclideanSpace ℝ (Fin d) =>
…

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