OAI/Analysis/PlanarPacking/GaussianSeries.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpPlanar.gaussian_shift_poissonline 9 - lemma
OAI.SharpPlanar.integer_gaussian_summableline 36 - lemma
OAI.SharpPlanar.real_integer_gaussian_summableline 42 - lemma
OAI.SharpPlanar.gaussian_scale_half_productline 46 - lemma
OAI.SharpPlanar.phase_gaussian_summableline 59