OAI/Probability/GaussianInformation/Dyadic/GaussianTails.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.gaussian_exp_square_integral line 18
2. lemma OAI.RepeatedLocalization.sqrt_two_le_exp_half line 41
3. lemma OAI.RepeatedLocalization.gaussian_scalar_scaled_exp_le line 47
4. lemma OAI.RepeatedLocalization.stdGaussian_inner_eq_scaled line 62
5. lemma OAI.RepeatedLocalization.stdGaussian_inner_exp_le line 73
6. lemma OAI.RepeatedLocalization.iidGaussian_linear_exp_le line 82
7. lemma OAI.RepeatedLocalization.gaussianRows_exp_square_le line 90
8. lemma OAI.RepeatedLocalization.gaussianRows_tail line 108