OAI/Probability/InvariantIsing/Cavity/CavityResidualFinite.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positivity and finiteness of the actual residual-integrated normalizer.

  1. lemma OAI.InvariantIsing.measurable_cavityLeafSum_joint line 13
  2. lemma OAI.InvariantIsing.measurable_cavityLeafSum line 22
  3. theorem OAI.InvariantIsing.cavity_residual_partition_pos_finite line 26
  4. lemma OAI.InvariantIsing.cavity_residual_partition_leaf_integrable line 81

    Source documentation

    Finiteness of the actual residual partition entails precisely the backward-quadratic leaf exponential integrability used by its tilted law.

    lemma cavity_residual_partition_leaf_integrable {d : ℕ} (n : ℕ)
    (K R : Matrix (Fin d) (Fin d) ℝ) (hK : K.IsHermitian) (hR : R.PosSemidef)
    (hQ : (cavityFactorPrecision K (CFC.sqrt R)).PosDef)
    (s : EuclideanSpace ℝ (Fin d)) (V : NoiseTree (EuclideanSpace ℝ (Fin d)) n)
    (hZ : cavityResidualPartition n K R s V < ∞) :
    Integrable (fun v => Real.exp (⟪cavityLeafSum n s v,
      Matrix.toEuclideanCLM (𝕜 := ℝ) (cavityBackwardQuadratic K R)
…

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