OAI/Analysis/PlanarPacking/FourierPairSupport.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpPlanar.gaussianCoeff line 15
  2. def OAI.SharpPlanar.spectralGaussian line 18
  3. lemma OAI.SharpPlanar.gaussianCoeff_re line 21
  4. lemma OAI.SharpPlanar.gaussianCoeff_re_pos line 24
  5. lemma OAI.SharpPlanar.spectralGaussian_norm line 28
  6. lemma OAI.SharpPlanar.spectralGaussian_continuous line 36
  7. lemma OAI.SharpPlanar.poisson_gaussian_plane line 40
  8. lemma OAI.SharpPlanar.gaussianCoeff_ne line 45
  9. lemma OAI.SharpPlanar.gaussianCoeff_lambda line 50
  10. lemma OAI.SharpPlanar.z_lambda_relation line 60
  11. lemma OAI.SharpPlanar.gaussianCoeff_exponent line 75
  12. lemma OAI.SharpPlanar.spectralGaussian_fourier line 86
  13. lemma OAI.SharpPlanar.spectralGaussian_integrable line 99
  14. lemma OAI.SharpPlanar.gaussian_damping_integrable line 105
  15. lemma OAI.SharpPlanar.spectralGaussian_joint_integrable line 109
  16. lemma OAI.SharpPlanar.spectralGaussian_fourier_integral line 127
  17. lemma OAI.SharpPlanar.fourier_integrable line 155
  18. lemma OAI.SharpPlanar.fourier_conj_even line 160
  19. lemma OAI.SharpPlanar.complex_re_as_sum line 175
  20. lemma OAI.SharpPlanar.fourier_integrable_exp line 178
  21. lemma OAI.SharpPlanar.fourier_re_even line 190
  22. def OAI.SharpPlanar.gaussianSpectral line 210
  23. lemma OAI.SharpPlanar.gaussianSpectral_integrable line 213
  24. lemma OAI.SharpPlanar.gaussianSpectral_even line 219
  25. lemma OAI.SharpPlanar.gaussianSpectral_eq line 223
  26. lemma OAI.SharpPlanar.gaussianSpectral_fourier line 237
  27. lemma OAI.SharpPlanar.gaussianSpectral_dirac_fourier line 247
  28. lemma OAI.SharpPlanar.density_piece_integrable line 253
  29. lemma OAI.SharpPlanar.fourier_add_integrable line 262
  30. lemma OAI.SharpPlanar.fourier_sum_integrable line 268
  31. def OAI.SharpPlanar.qComplex line 275
  32. lemma OAI.SharpPlanar.qComplex_integrable line 284
  33. lemma OAI.SharpPlanar.qComplex_even line 293
  34. lemma OAI.SharpPlanar.qComplex_re line 296
  35. lemma OAI.SharpPlanar.qComplex_fourier line 302
  36. lemma OAI.SharpPlanar.qSchwartz_fourier line 356