OAI/Probability/Renewal/Concentration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HoneycombLocal.AnnulusData.original_normalized line 11
2. lemma OAI.HoneycombLocal.lattice_mass_upper_of_envelope line 32
3. theorem OAI.HoneycombLocal.local_concentration line 57
4. theorem OAI.HoneycombLocal.annular_mass_and_concentration line 109