OAI/Geometry/LatticeCovering/Marginals.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SingleLatticeCovering.Prekopa.compact_volume_E line 17
2. lemma OAI.SingleLatticeCovering.Prekopa.scalarLogConcave_cap_volume_E line 36
3. lemma OAI.SingleLatticeCovering.Prekopa.scalarLogConcave_uniform_cap line 49
4. lemma OAI.SingleLatticeCovering.Prekopa.norm_fourth_le_sum line 59
5. lemma OAI.SingleLatticeCovering.Prekopa.fourth_norm_of_coordinates line 68
6. lemma OAI.SingleLatticeCovering.Prekopa.paley_zygmund_quarter line 84
7. lemma OAI.SingleLatticeCovering.Prekopa.uniform_body_fourth line 128
8. lemma OAI.SingleLatticeCovering.Prekopa.fourthMomentConstant_pos line 146
9. lemma OAI.SingleLatticeCovering.Prekopa.uniform_body_radius_lower line 150
10. lemma OAI.SingleLatticeCovering.GaussianDensity.scaled_gaussian_law line 180
11. lemma OAI.SingleLatticeCovering.GaussianDensity.measurable_mixture_kernel line 197
12. lemma OAI.SingleLatticeCovering.GaussianDensity.integrable_mixture_kernel line 206
13. lemma OAI.SingleLatticeCovering.GaussianDensity.mixture_integrable line 218
14. lemma OAI.SingleLatticeCovering.GaussianDensity.mixture_integral line 223
15. lemma OAI.SingleLatticeCovering.GaussianDensity.mixture_set_integral line 233
16. lemma OAI.SingleLatticeCovering.GaussianDensity.density_set_integral line 244
17. lemma OAI.SingleLatticeCovering.GaussianDensity.integrable_translated_density line 264
18. lemma OAI.SingleLatticeCovering.GaussianDensity.integral_translated_density line 269
19. lemma OAI.SingleLatticeCovering.GaussianDensity.integrable_convolution_kernel line 275
20. lemma OAI.SingleLatticeCovering.GaussianDensity.convolution_integrable line 289
21. lemma OAI.SingleLatticeCovering.GaussianDensity.convolution_integral line 295
22. lemma OAI.SingleLatticeCovering.GaussianDensity.neg_log_one_sub_le line 312
23. lemma OAI.SingleLatticeCovering.GaussianDensity.log_one_add_ge line 324
24. lemma OAI.SingleLatticeCovering.GaussianDensity.gaussian_chernoff_upper line 333
25. lemma OAI.SingleLatticeCovering.GaussianDensity.gaussian_chernoff_lower line 348
26. lemma OAI.SingleLatticeCovering.GaussianDensity.gaussian_norm_sq_upper line 364
27. lemma OAI.SingleLatticeCovering.GaussianDensity.gaussian_norm_sq_lower line 372
28. lemma OAI.SingleLatticeCovering.GaussianDensity.norm_scaled_sq line 390
29. lemma OAI.SingleLatticeCovering.GaussianDensity.density_small_ball_lower line 394
30. lemma OAI.SingleLatticeCovering.GaussianDensity.density_large_ball_lower line 412
31. lemma OAI.SingleLatticeCovering.GaussianDensity.mixture_scale_small line 431
32. lemma OAI.SingleLatticeCovering.GaussianDensity.mixture_scale_large line 455
33. lemma OAI.SingleLatticeCovering.GaussianDensity.stdGaussian_norm_second line 487
34. lemma OAI.SingleLatticeCovering.GaussianDensity.density_tail_markov line 508
35. lemma OAI.SingleLatticeCovering.GaussianDensity.mixture_tail_markov line 526
36. lemma OAI.SingleLatticeCovering.Prekopa.logConcave_smoothed_volume_E line 557
37. lemma OAI.SingleLatticeCovering.Prekopa.logConcave_smoothed_uniform line 576
38. def OAI.SingleLatticeCovering.GaussianProjection.colLinear line 590
39. def OAI.SingleLatticeCovering.GaussianProjection.normalizedProjection line 600
40. lemma OAI.SingleLatticeCovering.GaussianProjection.normalizedProjection_kernel line 604
41. lemma OAI.SingleLatticeCovering.GaussianProjection.logConcave_normalizedProjection line 614