OAI/Probability/DilutedSpin/PhysicalOverlapLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.UniversalDictionary.physicalOverlapLimsup line 15
2. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalOverlapLimsup_nonneg line 19
3. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalOverlapLimsup_le_one line 25
4. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalOverlapLimsup_bound line 31
5. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalOverlapLimsup_antitone line 47
6. lemma OAI.DilutedSpinGlass.UniversalDictionary.eventually_large_overlap_grid line 69
7. theorem OAI.DilutedSpinGlass.UniversalDictionary.physicalOverlapLimsup_tendsto line 79

   Source documentation

   All root, auxiliary and thermal randomness are concentrated. Branch depths alone are averaged; the topology and model are arbitrary and unchanged.

   theorem physicalOverlapLimsup_tendsto (M : Model p) (C H : ℝ)
       (Ns : ℕ → ℕ → ℕ) (us : (L : ℕ) → ℕ → Spec L×ℕ → ℝ)
       (hcontrol : ∀ L, FullShapeControl M C H L (Ns L) (us L))
       (S : ReducedTopology) {η : ℝ} (hη : 0<η) :
       Tendsto (fun L => physicalOverlapLimsup M C H L (Ns L) (us L) S η) atTop (𝓝 0) := by
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl, OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.UniversalDictionary.physicalOverlapLimsup