OAI/Probability/SKGap/Localization/RareCoordinate.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.gaussian_standard_subgaussian line 12
2. lemma OAI.SKGap.gaussian_observation_small line 19
3. def OAI.SKGap.rareCount line 51
4. lemma OAI.SKGap.rareCount_measurable line 55
5. lemma OAI.SKGap.rareCount_bounds line 64
6. lemma OAI.SKGap.rareCount_exp_integral line 72
7. theorem OAI.SKGap.rareCount_tail line 88