InsertionCoefficient.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.insertionCoefficient line 13
Source documentation
The actual independent index/fresh-label sampling for a fixed old replica array. A fresh label is one whole tree sample, not a new draw at each leaf.
```
noncomputable def insertionCoefficient {Z : Type} [Fintype Z] {p n N : ℕ} [NeZero N]
    (M : Model p) (old : Fin N → Fin n → Spin) (Q : FiniteLaw Z)
    (x : Z → Fin n → ℝ) (sel : Fin p → Bool) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FiniteLaw
lemma OAI.DilutedSpinGlass.insertionCoefficient_eq_raw line 22
lemma OAI.DilutedSpinGlass.insertionCoefficient_combination_nonneg line 53

lemma OAI.DilutedSpinGlass.expected_insertionCoefficient_nonneg line 64

Source documentation

The coefficient sign remains valid after sampling the old tilted tree; its sampling law is common to the bond, cavity and real insertions.

lemma expected_insertionCoefficient_nonneg {Ω Z : Type} [Fintype Ω] [Fintype Z]
    {p n N : ℕ} [NeZero N] (M : Model p) (hM : Admissible M) (hn : 1≤n)
    (P : FiniteLaw Ω) (old : Ω → Fin N → Fin n → Spin)
    (Q : FiniteLaw Z) (x : Z → Fin n → ℝ) (j : Fin p) :
    0 ≤ P.expect (fun w => insertionCoefficient M (old w) Q x (fun _ => true)) -
      (p:ℝ)*P.expect (fun w => insertionCoefficient M (old w) Q x (fun l => decide (l=j))) +
      ((p-1:ℕ):ℝ)*P.expect (fun w => insertionCoefficient M (old w) Q x (fun _ => false)) := by
…

Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.Admissible, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.insertionCoefficient