OAI/Probability/DilutedSpin/InsertionPoissonAlgebra.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.poisson_average_bound line 10
2. lemma OAI.DilutedSpinGlass.poisson_average_integrable line 18
3. lemma OAI.DilutedSpinGlass.double_limit_two line 24
4. def OAI.DilutedSpinGlass.UniversalDictionary.insertionPoisson line 50
5. def OAI.DilutedSpinGlass.UniversalDictionary.trialPoisson line 55
6. lemma OAI.DilutedSpinGlass.UniversalDictionary.insertionPoisson_comparison_bound line 60