OAI/Analysis/PlanarPacking/LatticeGaussian.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpPlanar.latticePoint line 10
  2. lemma OAI.SharpPlanar.latticePoint_zero line 11
  3. lemma OAI.SharpPlanar.latticePoint_norm line 14
  4. lemma OAI.SharpPlanar.thetaKernel_lattice line 20
  5. def OAI.SharpPlanar.spectralParameter line 27
  6. lemma OAI.SharpPlanar.spectralParameter_re line 28
  7. lemma OAI.SharpPlanar.spectralParameter_pos line 30
  8. lemma OAI.SharpPlanar.spectralParameter_ne line 32
  9. lemma OAI.SharpPlanar.gaussianCoeff_parameter line 36
  10. lemma OAI.SharpPlanar.spectralGaussian_lattice line 39
  11. lemma OAI.SharpPlanar.spectralGaussian_fourier_lattice line 43
  12. lemma OAI.SharpPlanar.spectralGaussian_hex_poisson line 54
  13. def OAI.SharpPlanar.latticeDamping line 59
  14. lemma OAI.SharpPlanar.latticeDamping_nonneg line 61
  15. lemma OAI.SharpPlanar.latticeDamping_summable line 62
  16. lemma OAI.SharpPlanar.lattice_spectral_bound line 68
  17. lemma OAI.SharpPlanar.lattice_fourier_spectral_bound line 70