OAI/Probability/DilutedSpin/RandomInsertion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.integral_fullRootLaw_reordered line 11
2. lemma OAI.DilutedSpinGlass.count_linear_le_quadratic line 29
3. lemma OAI.DilutedSpinGlass.UniversalDictionary.randomInsertion_comparison line 46
4. theorem OAI.DilutedSpinGlass.UniversalDictionary.randomInsertion_comparison_tendsto line 68

   Source documentation

   The bounded-insertion limit is uniform in independent physical disorder; the physical law is integrated without exchanging the two ordered limits.

   theorem randomInsertion_comparison_tendsto (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))
       (a : ℕ) (μ : Measure X) [IsProbabilityMeasure μ]
       (F : X → (Fin a → Spin) → ℝ) (hFm : Measurable F) {D : ℝ}
       (hD : 0≤D) (hF : ∀ x s, |F x s|≤D) :
       Tendsto (fun L => limsup (fun n =>
         |(∫ x, reservoirInsertion M C H (Ns L n+1) L (us L n) a (F x) ∂μ)-
           (∫ x, trialLog L (reservoirTrialLaw M C H (Ns L n+1) L (us L n))
             (fun i => gridExponents L i.castSucc) (FiniteLaw.spinLog (F x)) ∂μ)|) atTop) atTop (𝓝 0) := by
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.UniversalDictionary.reservoirInsertion, OAI.DilutedSpinGlass.trialLog, OAI.DilutedSpinGlass.UniversalDictionary.reservoirTrialLaw, OAI.DilutedSpinGlass.UniversalDictionary.gridExponents, OAI.DilutedSpinGlass.FiniteLaw.spinLog