OAI/Probability/DilutedSpin/CompoundPoisson.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.compoundPoisson line 13

   Source documentation

   The law of the sum of iid marks with an independent Poisson count.

   noncomputable def compoundPoisson (r : ℝ≥0) (μ : Measure E) : Measure E :=
   …

2. instance OAI.DilutedSpinGlass.compoundPoisson_prob line 17
3. lemma OAI.DilutedSpinGlass.charFunDual_iid_sum line 26
4. lemma OAI.DilutedSpinGlass.charFunDual_compoundPoisson line 34