OAI/Probability/DilutedSpin/SpinMarginal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.FiniteLaw.uniform_cons_expect line 9
2. lemma OAI.DilutedSpinGlass.FiniteLaw.exp_logMean_one line 23
3. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.mark_eq_pathMap line 37
4. def OAI.DilutedSpinGlass.HeterogeneousMarks.terminalRoot line 46
5. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalRoot_eq_backward line 53
6. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalRoot_marginal line 68
7. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalRoot_spin_marginal line 89

   Source documentation

   Exact new-spin marginalization at the final exponent1.

   lemma terminalRoot_spin_marginal
       (Q : (i : I) → Fin (L+1) → FiniteLaw (A i)) (m : Fin (L+1) → ℝ)
       (hm : m (Fin.last L)=1) (E : (Fin N → Spin) → ℝ) (G : (Fin (N+1) → Spin) → ℝ)
       (roots : Fin k → I) (ψ : (i : I) → (Fin N → Spin) → FinitePath (A i) (L+1) → ℝ) :
       terminalRoot (fun _ : Fin (N+1) => false) FiniteLaw.uniform Q m
         (fun σ => E (fun i => σ i.succ)+G σ) roots (fun i σ a => ψ i (fun j => σ j.succ) a) =
       terminalRoot (fun _ : Fin N => false) FiniteLaw.uniform Q m
         (fun σ => E σ+(FiniteLaw.uniform : FiniteLaw Spin).logMean 1 (fun ε => G (Fin.cons ε σ))) roots ψ := by
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.terminalRoot, OAI.DilutedSpinGlass.FiniteLaw.uniform, OAI.DilutedSpinGlass.logMean