OAI/Probability/InvariantIsing/Cavity/CavityQuadraticNormalizer.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.cavityDeterminantStep line 14
2. def OAI.InvariantIsing.cavityQuadraticValue line 18
3. lemma OAI.InvariantIsing.measurable_cavityQuadraticValue line 25
4. lemma OAI.InvariantIsing.cavityQuadraticValue_terminal line 31
5. lemma OAI.InvariantIsing.cavityQuadraticValue_root_integrable line 39
6. lemma OAI.InvariantIsing.cavityQuadraticValue_root_integral line 52
7. lemma OAI.InvariantIsing.cavityQuadraticStepWeight_telescoping line 62
8. lemma OAI.InvariantIsing.cavity_quadratic_step_fractional_moment line 73
9. theorem OAI.InvariantIsing.cavity_quadratic_cascade_log_integral line 95

   Source documentation

   Positivity, logarithmic integrability and the exact deterministic mean of the finite quadratic cascade normalizer.

   theorem cavity_quadratic_cascade_log_integral {d : ℕ} (n : ℕ)
       (K : Matrix (Fin d) (Fin d) ℝ)
       (H S : ℕ → Matrix (Fin d) (Fin d) ℝ) (b : ℕ → ℝ)
       (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)
       (s : EuclideanSpace ℝ (Fin d)) :
       let μ := cavityGaussianMarks S
   …

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