PhysicalInsertionLimit.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.UniversalDictionary.logSeries_tail_tendsto line 13
lemma OAI.DilutedSpinGlass.UniversalDictionary.reservoirTrialLog_bound line 18
theorem OAI.DilutedSpinGlass.UniversalDictionary.reservoirInsertion_comparison_tendsto line 27
Source documentation
Every uniformly bounded finite insertion has vanishing comparison error in the manuscript's ordered limits, on the single controlling physical sequence.
```
theorem reservoirInsertion_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 : ℕ) (F : (Fin a → Spin) → ℝ) {D : ℝ} (hD : 0≤D) (hF : ∀ s, |F s|≤D) :
    Tendsto (fun L => limsup (fun n =>
      |reservoirInsertion M C H (Ns L n+1) L (us L n) a F-
        trialLog L (reservoirTrialLaw M C H (Ns L n+1) L (us L n))
          (fun i => gridExponents L i.castSucc) (FiniteLaw.spinLog F)|) 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