OAI/Geometry/LatticeCovering/GaussianMoments.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SingleLatticeCovering.Assembly.all_dimensions_main_reduction_circuits line 47
  2. theorem OAI.SingleLatticeCovering.Assembly.main_reduction_to_EK_via_circuits line 71
  3. lemma OAI.SingleLatticeCovering.Isotropization.coordinate_memLp line 125
  4. lemma OAI.SingleLatticeCovering.Isotropization.isotropic_coordinate_second line 130
  5. lemma OAI.SingleLatticeCovering.Isotropization.isotropic_norm_sq line 136
  6. lemma OAI.SingleLatticeCovering.GaussianProjection.integral_norm_le_sqrt_second line 155
  7. lemma OAI.SingleLatticeCovering.GaussianProjection.inner_memLp_two line 164
  8. lemma OAI.SingleLatticeCovering.GaussianProjection.isotropic_abs_inner_integral line 169
  9. lemma OAI.SingleLatticeCovering.GaussianProjection.isotropic_norm_integral line 178
  10. lemma OAI.SingleLatticeCovering.GaussianProjection.exp_negative_lipschitz line 184
  11. def OAI.SingleLatticeCovering.GaussianProjection.radialGaussianAverage line 200
  12. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussianKernel_bounded line 203
  13. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussianKernel_integrable line 209
  14. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussianKernel_covariance_bound line 214
  15. def OAI.SingleLatticeCovering.GaussianProjection.phase line 235
  16. lemma OAI.SingleLatticeCovering.GaussianProjection.norm_phase line 238
  17. lemma OAI.SingleLatticeCovering.GaussianProjection.charFun_phase line 241
  18. lemma OAI.SingleLatticeCovering.GaussianProjection.phase_gaussian_integral line 245
  19. lemma OAI.SingleLatticeCovering.GaussianProjection.phase_product_integrable line 256
  20. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussian_char_average line 262
  21. lemma OAI.SingleLatticeCovering.GaussianProjection.phase_sub line 271
  22. lemma OAI.SingleLatticeCovering.GaussianProjection.charFun_differenceLaw line 277
  23. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussian_char_secondMoment line 290
  24. lemma OAI.SingleLatticeCovering.GaussianProjection.charFun_gaussian_integrable line 313
  25. lemma OAI.SingleLatticeCovering.GaussianProjection.charFun_gaussian_sq_integrable line 318
  26. lemma OAI.SingleLatticeCovering.GaussianProjection.complex_center_sq line 325
  27. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussian_char_variance_identity line 331
  28. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussianKernel_prod_integrable line 353
  29. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussian_char_variance_kernel line 358
  30. lemma OAI.SingleLatticeCovering.GaussianProjection.abs_inner_prod_integrable line 370
  31. lemma OAI.SingleLatticeCovering.GaussianProjection.isotropic_abs_inner_prod_integral line 377
  32. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussian_char_variance_bound line 388
  33. abbrev OAI.SingleLatticeCovering.GaussianProjection.MatrixSpace line 410
  34. def OAI.SingleLatticeCovering.GaussianProjection.rowApply line 412
  35. def OAI.SingleLatticeCovering.GaussianProjection.colApply line 415
  36. def OAI.SingleLatticeCovering.GaussianProjection.tensor line 418
  37. lemma OAI.SingleLatticeCovering.GaussianProjection.continuous_rowApply line 421
  38. lemma OAI.SingleLatticeCovering.GaussianProjection.continuous_colApply line 425
  39. lemma OAI.SingleLatticeCovering.GaussianProjection.inner_colApply line 429
  40. lemma OAI.SingleLatticeCovering.GaussianProjection.inner_rowApply line 441
  41. lemma OAI.SingleLatticeCovering.GaussianProjection.norm_tensor_sq line 451
  42. lemma OAI.SingleLatticeCovering.GaussianProjection.rowApply_gaussian_law line 456
  43. lemma OAI.SingleLatticeCovering.GaussianProjection.radialGaussianAverage_nonneg line 474
  44. lemma OAI.SingleLatticeCovering.GaussianProjection.radialGaussianAverage_le_one line 477
  45. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussian_char_mean_deviation line 485
  46. lemma OAI.SingleLatticeCovering.GaussianProjection.gaussian_matrix_char_deviation line 502
  47. lemma OAI.SingleLatticeCovering.GaussianProjection.isotropic_stdGaussian line 524
  48. lemma OAI.SingleLatticeCovering.GaussianProjection.continuous_radialGaussianAverage line 531
  49. lemma OAI.SingleLatticeCovering.GaussianProjection.matrix_char_deviation_bound line 540
  50. lemma OAI.SingleLatticeCovering.GaussianProjection.continuous_matrix_char_deviation line 550
  51. lemma OAI.SingleLatticeCovering.GaussianProjection.matrix_char_deviation_integrable line 558
  52. def OAI.SingleLatticeCovering.GaussianProjection.matrixSmoothingError line 565
  53. lemma OAI.SingleLatticeCovering.GaussianProjection.matrixSmoothingError_nonneg line 568
  54. lemma OAI.SingleLatticeCovering.GaussianProjection.matrixSmoothingError_integrable line 571
  55. lemma OAI.SingleLatticeCovering.GaussianProjection.matrixSmoothingError_mean line 575
  56. def OAI.SingleLatticeCovering.GaussianProjection.smoothedProjection line 594
  57. def OAI.SingleLatticeCovering.GaussianProjection.radialSmoothedModel line 598
  58. lemma OAI.SingleLatticeCovering.GaussianProjection.phase_projected_sub line 601
  59. lemma OAI.SingleLatticeCovering.GaussianProjection.projected_phase_integrable line 608
  60. lemma OAI.SingleLatticeCovering.GaussianProjection.smoothedProjection_fourier line 617
  61. lemma OAI.SingleLatticeCovering.GaussianProjection.smoothedProjection_uniform_error line 627
  62. theorem OAI.SingleLatticeCovering.GaussianProjection.exists_uniform_smoothed_projection line 654