OAI/Probability/DilutedSpin/PoissonSiteThinning.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.compoundPoisson_uniform_indicator_at line 12

   Source documentation

   Poisson thinning for independent uniform categorical choices.

   lemma compoundPoisson_uniform_indicator_at (r : ℝ≥0) (p : ℕ) [NeZero p] (s : Fin p) :
       compoundPoisson r (Measure.map (fun a : Fin p => if a=s then (1:ℝ) else 0)
         (finiteUniform (Fin p))) = compoundPoisson (r/p) (Measure.dirac (1:ℝ)) := by
   …

   Mentions: OAI.DilutedSpinGlass.compoundPoisson, OAI.DilutedSpinGlass.finiteUniform

2. def OAI.DilutedSpinGlass.successCountAt line 39
3. lemma OAI.DilutedSpinGlass.map_poisson_successCountAt line 42
4. lemma OAI.DilutedSpinGlass.selectedCount_eq_successCountAt line 65