OAI/Probability/DilutedSpin/SpinBaseComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.FiniteLaw.pi_uniform line 11
2. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_uniform line 17
3. theorem OAI.DilutedSpinGlass.SizeCoupling.spinMean_one line 29

   Source documentation

   Exact entropy normalization, not merely an asymptotic comparison.

   theorem spinMean_one {N p k l r : ℕ} [NeZero N] {A : Fin l → Type}
       [∀ i, Fintype (A i)]
       (Q : (i : Fin l) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
       (hm : ∀ j, m j ≠ 0) (hend : m (Fin.last r) = 1)
       (theta : Fin k → InteractionSample p) (h : Fin N → ℝ) :
       spinMean Q m theta h (fun _ _ _ => 1) = indexAverage theta h-N*Real.log 2 := by
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.SizeCoupling.spinMean, OAI.DilutedSpinGlass.indexAverage

4. theorem OAI.DilutedSpinGlass.SizeCoupling.spinMean_base_distance line 41
5. lemma OAI.DilutedSpinGlass.SizeCoupling.integrate_close line 61