OAI/Analysis/PlanarPacking/LatticePoisson.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SharpPlanar.HasLatticePoisson line 9
2. lemma OAI.SharpPlanar.HasLatticePoisson.add line 14
3. lemma OAI.SharpPlanar.HasLatticePoisson.zero line 25
4. lemma OAI.SharpPlanar.HasLatticePoisson.finset_sum line 32
5. lemma OAI.SharpPlanar.gaussianSpectral_hasPoisson line 41
6. lemma OAI.SharpPlanar.gaussianSpectral_dirac_hasPoisson line 47
7. lemma OAI.SharpPlanar.density_piece_hasPoisson line 51
8. lemma OAI.SharpPlanar.qComplex_hasPoisson line 61
9. lemma OAI.SharpPlanar.qk_lattice_summable line 75
10. lemma OAI.SharpPlanar.qk_lattice_poisson line 83
11. lemma OAI.SharpPlanar.pair_lattice_poisson line 90