OAI/Probability/DilutedSpin/CountBridgeTools.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.cavity_split_lipschitz_bound line 20

   Source documentation

   The actual finite-volume Poisson cavity split, with only the discarded multiple-new-index energy as error. The bound is uniform over the rooted finite power-mean functional, its old disorder and every auxiliary level.

   lemma cavity_split_lipschitz_bound (α : ℝ≥0) (q N : ℕ) [NeZero N]
       (V : X × (Fin (q+1) → Fin (N+1)) → E) (hV : Measurable V)
       {D : ℝ} (hD : 0≤D) (hbound : ∀ z,‖V z‖≤D)
       {f : E → ℝ} (hf : LipschitzWith 1 f) :
       |(∫ x, f x ∂compoundPoisson (α*(N+1))
           (Measure.map V (μ.prod (finiteUniform (Fin (q+1) → Fin (N+1))))))-
         (∫ x, f x ∂(compoundPoisson (reservoirRate α q N)
           (Measure.map (fun z : X × (Fin (q+1) → Fin N) => V (z.1,fun i => (z.2 i).succ))
             (μ.prod (finiteUniform (Fin (q+1) → Fin N)))) ∗
         compoundPoisson (oneNewRate α q N)
           (Measure.map (fun z : X × (Fin (q+1) × (Fin q → Fin N)) =>
               V (z.1,z.2.1.insertNth 0 (fun i => (z.2.2 i).succ)))
   …

   Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.compoundPoisson, OAI.DilutedSpinGlass.finiteUniform, OAI.DilutedSpinGlass.reservoirRate, OAI.DilutedSpinGlass.oneNewRate

2. lemma OAI.DilutedSpinGlass.compoundPoisson_rate_limit line 41
3. lemma OAI.DilutedSpinGlass.FiniteLaw.integral_expect line 62
4. lemma OAI.DilutedSpinGlass.FiniteLaw.integral_expect_bounded line 68
5. lemma OAI.DilutedSpinGlass.SizeCoupling.measurable_spinRoot line 79
6. lemma OAI.DilutedSpinGlass.SizeCoupling.spinRoot_bound line 94