OAI/Probability/DilutedSpin/PoissonInsertionLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.UniversalDictionary.poissonInsertionOn_comparison_tendsto line 14

   Source documentation

   Poisson many distinct inserted labels, with their physical disorder, obey the same ordered full-shape limit. The linear Poisson tail is retained, not replaced by a bound on the number of cavity interactions.

   lemma poissonInsertionOn_comparison_tendsto
       {ι X : ℕ → Type} [∀ k,Fintype (ι k)] [∀ k,MeasurableSpace (X k)]
       {p : ℕ} (M : Model p) (hα : 0<M.alpha) (C H : ℝ)
       (Ns : ℕ → ℕ → ℕ) (hNs : ∀ L,Tendsto (Ns L) atTop atTop)
       (us : (L : ℕ) → ℕ → Spec L×ℕ → ℝ)
       (hcontrol : ∀ L,FullShapeControl M C H L (Ns L) (us L))
       (μ : (k : ℕ) → Measure (X k)) [∀ k,IsProbabilityMeasure (μ k)]
       (F : (k : ℕ) → X k → (ι k → Spin) → ℝ) (hFm : ∀ k,Measurable (F k))
       {B D : ℝ} (hB : 0≤B) (hD : 0≤D)
       (hF : ∀ k x s,|F k x s|≤B+D*k) (ρ : ℝ≥0) :
       Tendsto (fun L => limsup (fun n => ∫ k,
         |(∫ x,reservoirInsertionOn M C H (Ns L n+1) L (us L n) (F k x) ∂μ k)-
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.UniversalDictionary.reservoirInsertionOn