CavityResidualLeafLaw.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The residual factorization for the actual finite quadratic cascade.

theorem OAI.InvariantIsing.cavity_quadratic_residual_leaf_law line 15

Source documentation

For every tree with finite actual normalizer, integrating and centering its ordinary residual leaves the precise quadratic tilted leaf law.

theorem cavity_quadratic_residual_leaf_law {d : ℕ} (n : ℕ)
    (K : Matrix (Fin d) (Fin d) ℝ) (H : ℕ → Matrix (Fin d) (Fin d) ℝ) (b : ℕ → ℝ)
    (hK : K.transpose = K) (hR : (H n).PosSemidef)
    (hdet : IsUnit (1 - H n * K).det)
    (hQ : (cavityFactorPrecision K (CFC.sqrt (H n))).PosDef)
    (s : EuclideanSpace ℝ (Fin d)) (V : NoiseTree (EuclideanSpace ℝ (Fin d)) n)
    (hZ : cavityResidualPartition n K (H n) s V < ∞) :
    (normalizeMass (((noiseLeafKernel (EuclideanSpace ℝ (Fin d)) n V).prod
      (multivariateGaussian 0 (H n))).withDensity
        (fun p : NoiseLeaf (EuclideanSpace ℝ (Fin d)) n × EuclideanSpace ℝ (Fin d) =>
          ENNReal.ofReal (Real.exp (⟪cavityLeafSum n s p.1 + p.2,
            Matrix.toEuclideanCLM (𝕜 := ℝ) K (cavityLeafSum n s p.1 + p.2)⟫ / 2))))).map
…

Mentions: OAI.InvariantIsing.cavityFactorPrecision, OAI.InvariantIsing.cavityResidualPartition, OAI.InvariantIsing.cavityLeafSum