OAI/Probability/DilutedSpin/ConcreteReservoir.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DilutedSpinGlass.ConcreteReservoir.Site line 13
2. instance OAI.DilutedSpinGlass.ConcreteReservoir.siteNeZero line 14
3. def OAI.DilutedSpinGlass.ConcreteReservoir.readSpin line 18

   Source documentation

   N=0 is an irrelevant harmless extension; for every positive N this reads exactly the spin at the uniformly sampled original site.

   def readSpin {N : ℕ} (σ : Fin N → Spin) (i : Site N) : Spin :=
   …

   Mentions: OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.ConcreteReservoir.Site

4. lemma OAI.DilutedSpinGlass.ConcreteReservoir.readSpin_eq line 21
5. def OAI.DilutedSpinGlass.ConcreteReservoir.siteLaw line 30
6. instance OAI.DilutedSpinGlass.ConcreteReservoir.siteLaw_probability line 31
7. abbrev OAI.DilutedSpinGlass.ConcreteReservoir.Bond line 33
8. def OAI.DilutedSpinGlass.ConcreteReservoir.bondLaw line 34
9. instance OAI.DilutedSpinGlass.ConcreteReservoir.bondLaw_probability line 36
10. def OAI.DilutedSpinGlass.ConcreteReservoir.boundedPotential line 39
11. lemma OAI.DilutedSpinGlass.ConcreteReservoir.boundedPotential_bound line 42
12. lemma OAI.DilutedSpinGlass.ConcreteReservoir.measurable_boundedPotential line 45
13. def OAI.DilutedSpinGlass.ConcreteReservoir.markLaw line 58
14. instance OAI.DilutedSpinGlass.ConcreteReservoir.markLaw_probability line 59
15. def OAI.DilutedSpinGlass.ConcreteReservoir.siteObservable line 61
16. def OAI.DilutedSpinGlass.ConcreteReservoir.scoreError line 69

    Source documentation

    Literal full-root globally centered score for the physical iid-uniform Poisson reservoir, with bounded representatives equal to the original bounded physical variables almost surely. Every old dictionary term remains present.

    noncomputable def scoreError (M : Model p) (C H : ℝ) (j : K×ℕ) (N : ℕ) (u : K×ℕ → ℝ) : ℝ :=
    …

    Mentions: OAI.DilutedSpinGlass.Model

17. lemma OAI.DilutedSpinGlass.ConcreteReservoir.scoreError_nonneg line 76
18. theorem OAI.DilutedSpinGlass.ConcreteReservoir.scoreError_tendsto line 82

    Source documentation

    Concentration for these concrete model laws (not an assumed concentration interface) under the manuscript's bounded-stage hypotheses.

    theorem scoreError_tendsto (M : Model p) {C H c : ℝ} (hC : 0 ≤ C) (hH : 0 ≤ H) (hc : 0 < c)
        (hm : ∀ l, c ≤ m l) (hw : ∀ j, 0 < ν.real {j})
        (hD : ∀ q σ y, |D q σ y| ≤ 1) (hE : ∀ q σ y, |E q σ y| ≤ 1) (j : K×ℕ) :
        Filter.Tendsto (fun N => ∫ u, scoreError ν Q m D E M C H j N u
          ∂Measure.infinitePi (fun i : K×ℕ => intervalParameterLaw (probeLow i.2) (probeHigh i.2)))
          Filter.atTop (𝓝 0) := by
    …

    Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ConcreteReservoir.scoreError, OAI.DilutedSpinGlass.intervalParameterLaw, OAI.DilutedSpinGlass.probeLow, OAI.DilutedSpinGlass.probeHigh