OAI/Combinatorics/SparsestCut/GaussianTools.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniformSparsestCut.GaussianTools.subgaussian_abs_tail line 17
2. theorem OAI.UniformSparsestCut.GaussianTools.bounded_concentration line 33
3. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_cos_integrable line 86
4. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_cos line 92
5. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_linear_sin_integrable line 108
6. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_linear_sin line 118
7. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_vector_sin_integrable line 163
8. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_vector_sin line 168
9. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_inner_law line 177
10. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_inner_sq line 187
11. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_inner_subgaussian line 193
12. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_inner_tail line 204
13. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_real_exp_sq line 213
14. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_real_exp_sq_integrable line 238
15. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_exp_norm_sq line 245
16. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_exp_norm_sq_integrable line 264
17. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_norm_upper line 272
18. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_norm_lower line 302
19. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_norm_tail line 330
20. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_truncated_sq_bound line 354
21. lemma OAI.UniformSparsestCut.GaussianTools.gaussian_norm_sq_integrable line 398
22. def OAI.UniformSparsestCut.GaussianTools.truncate line 415
23. lemma OAI.UniformSparsestCut.GaussianTools.measurable_truncation_set line 419
24. lemma OAI.UniformSparsestCut.GaussianTools.measurable_tail_set line 422
25. lemma OAI.UniformSparsestCut.GaussianTools.integrable_truncate line 425
26. lemma OAI.UniformSparsestCut.GaussianTools.truncation_bias line 428
27. lemma OAI.UniformSparsestCut.GaussianTools.inner_sq_integrable line 451
28. lemma OAI.UniformSparsestCut.GaussianTools.truncation_covariance_bias line 459
29. lemma OAI.UniformSparsestCut.GaussianTools.truncation_fourier_bias line 468
30. lemma OAI.UniformSparsestCut.GaussianTools.truncate_fourier_bound line 483
31. lemma OAI.UniformSparsestCut.GaussianTools.truncate_covariance_bound line 497