OAI/Probability/InvariantIsing/Cavity/CavityResidualKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The ordinary residual, sampled independently for each replica, becomes independent of the tilted leaf after its centered Gaussian innovation map. It is not an additional level of the Poisson tree.

  1. lemma OAI.InvariantIsing.cavity_exp_mass_eq_scaled_tilt line 16
  2. lemma OAI.InvariantIsing.cavity_weighted_product_transport line 34
  3. lemma OAI.InvariantIsing.cavity_normalize_prod_right line 68
  4. theorem OAI.InvariantIsing.cavity_residual_joint_kernel line 82

    Source documentation

    The full leaf/residual Gibbs law factors after centering the ordinary residual. The first factor is the backward-quadratic leaf tilt, while the second is a Gaussian with covariance (I-HK)⁻¹H.

    theorem cavity_residual_joint_kernel {X : Type*} [MeasurableSpace X] [Nonempty X]
    {d : ℕ} (ν : Measure X) [IsProbabilityMeasure ν]
    (y : X → EuclideanSpace ℝ (Fin d)) (hy : Measurable y)
    (K H : Matrix (Fin d) (Fin d) ℝ) (hK : K.transpose = K) (hH : H.PosSemidef)
    (hdet : IsUnit (1 - H * K).det)
    (hQ : (cavityFactorPrecision K (CFC.sqrt H)).PosDef)
    (hI : Integrable (fun x => Real.exp
      (⟪y x, Matrix.toEuclideanCLM (𝕜 := ℝ) (cavityBackwardQuadratic K H) (y x)⟫ / 2)) ν) :
…

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