OAI/Probability/DilutedSpin/RawPatternIdentity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.rawReplicaMoment_eq_product line 11
2. lemma OAI.DilutedSpinGlass.freshPatternFeature_raw line 29
3. lemma OAI.DilutedSpinGlass.raw_mixedPatternMoment line 39
4. lemma OAI.DilutedSpinGlass.averaged_product_bound line 62

   Source documentation

   Averaging an inserted factor against arbitrary independent spin laws preserves the original uniform interaction bound.

   lemma averaged_product_bound {p : ℕ} (b : ℝ) (f : Fin p → Spin → ℝ)
       (h : ∀ s : Fin p → Spin,|b*∏ l,f l (s l)|≤1)
       (P : Fin p → FiniteLaw Spin) : |b*∏ l,(P l).expect (f l)|≤1 := by
   …

   Mentions: OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FiniteLaw