OAI/Probability/DilutedSpin/PhysicalSubtreeConcentration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeVariance line 15
2. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeVariance_realize line 26
3. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeVariance_nonneg line 31
4. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeVariance_le_one line 38
5. theorem OAI.DilutedSpinGlass.UniversalDictionary.physicalSubtree_limsup_tendsto line 46

   Source documentation

   The actual physical subsequence, not a newly assumed concentration law.

   theorem physicalSubtree_limsup_tendsto (M : Model p) (C H : ℝ)
       (Ns : ℕ → ℕ → ℕ) (us : (L : ℕ) → ℕ → Spec L×ℕ → ℝ)
       (hcontrol : ∀ L, FullShapeControl M C H L (Ns L) (us L)) (K k : ℕ) :
       Tendsto (fun L => limsup (fun n => qExpect (grid (L+1) 0 (L+1))
         (subtreePotential K (physicalTreeVariance M C H (Ns L n+1) L (us L n)))
         k (single (L+1))) atTop) atTop (𝓝 0) := by
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl, OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeVariance