OAI/Probability/GaussianInformation/Dyadic/SmallBalls.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.inv_pow_dyadic_majorant line 15
2. lemma OAI.RepeatedLocalization.dyadic_weight_product line 49
3. theorem OAI.RepeatedLocalization.inverseMoment_of_dyadic_tails line 57
4. theorem OAI.RepeatedLocalization.zeroSet_null_of_dyadic_tails line 99
5. theorem OAI.RepeatedLocalization.weightedMeasure_apply_le_sqrt line 126
6. theorem OAI.RepeatedLocalization.weightedMeasure_mass_le_one line 146