OAI/Probability/DilutedSpin/CompoundCoupling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.compoundPoisson_map_linear line 14
2. lemma OAI.DilutedSpinGlass.integrable_lipschitz_of_id line 24
3. lemma OAI.DilutedSpinGlass.integral_norm_sub_compound line 36
4. lemma OAI.DilutedSpinGlass.compoundPoisson_lipschitz_coupling line 53

   Source documentation

   A first-moment transport bound for the physical marked Poisson process. It also justifies deletion of all repeated-new-site bonds at their actual cost.

   lemma compoundPoisson_lipschitz_coupling [CompleteSpace E] (r : ℝ≥0) (μ : Measure (E×E))
       [IsProbabilityMeasure μ] (hi : Integrable id μ) {C : ℝ≥0} {f : E → ℝ}
       (hf : LipschitzWith C f) :
       |(∫ x, f x ∂compoundPoisson r (Measure.map Prod.fst μ))-
         (∫ x, f x ∂compoundPoisson r (Measure.map Prod.snd μ))| ≤
         C*r*(∫ z,‖z.1-z.2‖ ∂μ) := by
   …

   Mentions: OAI.DilutedSpinGlass.compoundPoisson