OAI/Probability/DilutedSpin/UpperReplicaPatterns.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.qLaw line 12
2. def OAI.DilutedSpinGlass.averagedFactor line 17
3. def OAI.DilutedSpinGlass.freshPatternLaw line 23

   Source documentation

   The finite law of spin patterns induced by one fresh message label on all replica leaves. The message label, including its root, is shared across leaves; only the final spin draws are conditionally independent.

   noncomputable def freshPatternLaw {Z : Type} [Fintype Z] {n : ℕ}
       (Q : FiniteLaw Z) (x : Z → Fin n → ℝ) : FiniteLaw (Fin n → Spin) :=
   …

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

4. lemma OAI.DilutedSpinGlass.freshPatternFeature line 27
5. def OAI.DilutedSpinGlass.oldPatternLaw line 38

   Source documentation

   Empirical pattern law of the old spin array at independently drawn sites.

   noncomputable def oldPatternLaw {N n : ℕ} [NeZero N]
       (s : Fin N → Fin n → Spin) : FiniteLaw (Fin n → Spin) :=
   …

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

6. lemma OAI.DilutedSpinGlass.oldPatternFeature line 42
7. lemma OAI.DilutedSpinGlass.mixedPatternMoment line 48