OAI/Probability/DilutedSpin/CavityIndex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.extensive_lower_bound line 12

   Source documentation

   A purely numerical telescope, used on the averaged pressure at sizes n+1.

   lemma extensive_lower_bound {P : ℕ → ℝ} {v : ℝ} {n : ℕ}
       (h : ∀ N, n ≤ N → v ≤ P (N+1)-P N) :
       ∀ N, n ≤ N → P n+((N:ℝ)-n)*v ≤ P N := by
   …

2. theorem OAI.DilutedSpinGlass.arbitrarily_large_low_increment line 25

   Source documentation

   Infinitely many low increments follow from the physical liminf and a vanishing normalized perturbation. No low-increment sequence is assumed.

   theorem arbitrarily_large_low_increment (P f : ℕ → ℝ)
       (hbelow : atTop.IsBoundedUnder (· ≥ ·) f)
       (habove : atTop.IsCoboundedUnder (· ≥ ·) f)
       (hnear : Tendsto (fun N => P N/((N:ℝ)+1)-f N) atTop (𝓝 0))
       {v : ℝ} (hv : liminf f atTop < v) (n : ℕ) :
       ∃ N, n ≤ N ∧ P (N+1)-P N ≤ v := by
   …

3. def OAI.DilutedSpinGlass.CavityGood line 64

   Source documentation

   Keep precisely the bonds meeting the new site at most once.

   def CavityGood {q N : ℕ} (x : Fin (q+1) → Fin (N+1)) : Prop :=
   …

   Mentions: OAI.DilutedSpinGlass.q

4. abbrev OAI.DilutedSpinGlass.CavityIndex line 67
5. def OAI.DilutedSpinGlass.cavityIndexMap line 70
6. lemma OAI.DilutedSpinGlass.cavityIndexMap_inr_zero_iff line 74
7. lemma OAI.DilutedSpinGlass.cavityIndexMap_good line 84
8. lemma OAI.DilutedSpinGlass.cavityIndexMap_injective line 92
9. lemma OAI.DilutedSpinGlass.cavityIndexMap_surjective_good line 123
10. def OAI.DilutedSpinGlass.cavityGoodEquiv line 142
11. instance OAI.DilutedSpinGlass.cavityGoodFintype line 149
12. lemma OAI.DilutedSpinGlass.sum_cavityGood line 152
13. lemma OAI.DilutedSpinGlass.sum_cavityKeep line 162