CavityRootInnovationLaw.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Independence of the common Gaussian root and retained innovation tree.

lemma OAI.InvariantIsing.cavity_root_tree_independent line 14

theorem OAI.InvariantIsing.cavity_quadratic_root_tree_law line 47

Source documentation

Root-dependent reweighting preserves the unchanged external root law. After the deterministic root rescaling, the innovation tree is independent of a centered Gaussian root with covariance J₀ S₀ J₀ᵀ.

theorem cavity_quadratic_root_tree_law {d : ℕ} (n : ℕ)
    (K : Matrix (Fin d) (Fin d) ℝ)
    (H S : ℕ → Matrix (Fin d) (Fin d) ℝ) (b : ℕ → ℝ)
    (S₀ : Matrix (Fin d) (Fin d) ℝ) (hS₀ : S₀.PosSemidef)
    (hK : K.transpose = K) (hH : ∀ i, (H i).transpose = H i)
    (hS : ∀ i, (S i).PosSemidef) (hb : ∀ i, 0 < b i)
    (hdet : ∀ i, IsUnit (1 - H i * K).det)
    (hΔ : ∀ i, H i - H (i + 1) = b i • S i)
    (hQ : ∀ i, (cavityFactorPrecision
      (b i • cavityBackwardQuadratic K (H (i + 1))) (CFC.sqrt (S i))).PosDef) :
    let μ := cavityGaussianMarks S
…

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