OAI/Probability/InvariantIsing/Cavity/CavityResidualPartition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.cavityResidualPartition line 15

   Source documentation

   The final Gaussian integral is an ordinary residual at each leaf, not an additional Poisson level.

   def cavityResidualPartition {d : ℕ} (n : ℕ)
       (K R : Matrix (Fin d) (Fin d) ℝ) (s : EuclideanSpace ℝ (Fin d))
       (V : NoiseTree (EuclideanSpace ℝ (Fin d)) n) : ℝ≥0∞ :=
   …

2. lemma OAI.InvariantIsing.cavity_residual_lintegral line 23
3. lemma OAI.InvariantIsing.cavityResidualPartition_eq_leafIntegral line 37
4. lemma OAI.InvariantIsing.cavity_noiseTreeTotal_pos_finite line 55
5. lemma OAI.InvariantIsing.cavity_residual_factor_log_eq line 66
6. lemma OAI.InvariantIsing.measurable_cavityResidualPartition line 94
7. theorem OAI.InvariantIsing.cavity_residual_partition_log_integral line 115

   Source documentation

   The complete source normalizer, including the last ordinary Gaussian integral and the common Gaussian root, is logarithmically integrable.

   theorem cavity_residual_partition_log_integral {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)
       (hbCascade : CascadeExponents n b)
       (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)
       (hR : (H n).PosSemidef)
   …

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