OAI/Geometry/LatticeCovering/GaussianSmoothing.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussian_matrix_char_average line 13
  2. lemma OAI.SingleLatticeCovering.GaussianProjection.matrix_phase_char_integrable line 25
  3. lemma OAI.SingleLatticeCovering.GaussianProjection.radialSmoothedModel_eq_average line 36
  4. def OAI.SingleLatticeCovering.GaussianProjection.radialSmoothedDensity line 44
  5. lemma OAI.SingleLatticeCovering.GaussianProjection.radialSmoothedDensity_nonneg line 47
  6. lemma OAI.SingleLatticeCovering.GaussianProjection.radialSmoothedDensity_cast line 52
  7. lemma OAI.SingleLatticeCovering.GaussianProjection.radialSmoothedModel_invariant line 56
  8. lemma OAI.SingleLatticeCovering.GaussianProjection.radialSmoothedDensity_norm_eq line 71
  9. lemma OAI.SingleLatticeCovering.GaussianProjection.smoothedProjection_real_uniform_error line 78
  10. lemma OAI.SingleLatticeCovering.GaussianProjection.continuous_smoothedProjection line 86
  11. lemma OAI.SingleLatticeCovering.GaussianProjection.smoothedProjection_le_one line 101
  12. lemma OAI.SingleLatticeCovering.GaussianProjection.continuous_smoothedProjection_y line 115
  13. lemma OAI.SingleLatticeCovering.GaussianProjection.continuous_smoothedProjection_g line 120
  14. lemma OAI.SingleLatticeCovering.GaussianProjection.norm_smoothedProjection_le line 127
  15. lemma OAI.SingleLatticeCovering.GaussianProjection.continuous_radialSmoothedDensity line 132
  16. abbrev OAI.SingleLatticeCovering.GaussianDensity.E line 156
  17. def OAI.SingleLatticeCovering.GaussianDensity.normalizer line 158
  18. def OAI.SingleLatticeCovering.GaussianDensity.density line 159
  19. def OAI.SingleLatticeCovering.GaussianDensity.law line 160
  20. lemma OAI.SingleLatticeCovering.GaussianDensity.normalizer_pos line 163
  21. lemma OAI.SingleLatticeCovering.GaussianDensity.density_pos line 166
  22. lemma OAI.SingleLatticeCovering.GaussianDensity.continuous_density line 169
  23. lemma OAI.SingleLatticeCovering.GaussianDensity.integrable_kernel line 172
  24. lemma OAI.SingleLatticeCovering.GaussianDensity.integral_kernel line 178
  25. lemma OAI.SingleLatticeCovering.GaussianDensity.integrable_density line 181
  26. lemma OAI.SingleLatticeCovering.GaussianDensity.integral_density line 183
  27. lemma OAI.SingleLatticeCovering.GaussianDensity.law_probability line 186
  28. lemma OAI.SingleLatticeCovering.GaussianDensity.integral_law line 193
  29. lemma OAI.SingleLatticeCovering.GaussianDensity.charFun_law line 202
  30. lemma OAI.SingleLatticeCovering.GaussianDensity.stdGaussian_eq_law line 224
  31. lemma OAI.SingleLatticeCovering.GaussianDensity.density_mul_exp line 240
  32. lemma OAI.SingleLatticeCovering.GaussianDensity.integrable_exp_norm_sq line 247
  33. lemma OAI.SingleLatticeCovering.GaussianDensity.integral_exp_norm_sq line 257
  34. lemma OAI.SingleLatticeCovering.GaussianDensity.normalizer_eq_exp line 263
  35. lemma OAI.SingleLatticeCovering.GaussianDensity.stdGaussian_laplace_norm_sq line 270
  36. lemma OAI.SingleLatticeCovering.GaussianDensity.stdGaussian_integrable_exp_norm_sq line 285
  37. lemma OAI.SingleLatticeCovering.GaussianDensity.integral_real_quadratic line 299
  38. lemma OAI.SingleLatticeCovering.GaussianDensity.normalizer_ratio_half line 312
  39. lemma OAI.SingleLatticeCovering.GaussianDensity.gaussian_convolution_kernel line 321
  40. lemma OAI.SingleLatticeCovering.GaussianProjection.colApply_gaussian_law line 352
  41. lemma OAI.SingleLatticeCovering.GaussianProjection.kernel_normalization line 370
  42. lemma OAI.SingleLatticeCovering.GaussianProjection.radialSmoothedDensity_mixture line 390
  43. lemma OAI.SingleLatticeCovering.GaussianProjection.normalized_radialSmoothedDensity_mixture line 416
  44. lemma OAI.SingleLatticeCovering.Prekopa.weighted_transport_inequality line 442
  45. theorem OAI.SingleLatticeCovering.Prekopa.positive_probability_lintegral line 463
  46. theorem OAI.SingleLatticeCovering.Prekopa.positive_integral line 511
  47. abbrev OAI.SingleLatticeCovering.Prekopa.RV line 544
  48. def OAI.SingleLatticeCovering.Prekopa.gaussianKernel line 546
  49. lemma OAI.SingleLatticeCovering.Prekopa.gaussianKernel_prod line 549
  50. lemma OAI.SingleLatticeCovering.Prekopa.gaussianKernel_pos line 553
  51. lemma OAI.SingleLatticeCovering.Prekopa.gaussianKernel_le_one line 555
  52. lemma OAI.SingleLatticeCovering.Prekopa.continuous_gaussianKernel line 560
  53. lemma OAI.SingleLatticeCovering.Prekopa.integrable_gaussianKernel line 564
  54. lemma OAI.SingleLatticeCovering.Prekopa.integral_gaussianKernel line 573
  55. lemma OAI.SingleLatticeCovering.Prekopa.gaussianKernel_cons line 579
  56. def OAI.SingleLatticeCovering.Prekopa.GaussianBound line 585
  57. lemma OAI.SingleLatticeCovering.Prekopa.GaussianBound.integrable line 588
  58. lemma OAI.SingleLatticeCovering.Prekopa.gaussian_slice_dominant line 594
  59. lemma OAI.SingleLatticeCovering.Prekopa.GaussianBound.integrable_slice line 602
  60. def OAI.SingleLatticeCovering.Prekopa.marginalOne line 611
  61. lemma OAI.SingleLatticeCovering.Prekopa.GaussianBound.continuous_marginalOne line 614
  62. lemma OAI.SingleLatticeCovering.Prekopa.marginalOne_positive line 627
  63. lemma OAI.SingleLatticeCovering.Prekopa.GaussianBound.for_marginalOne line 633
  64. lemma OAI.SingleLatticeCovering.Prekopa.integral_marginalOne line 653