OAI/NumberTheory/TwoPoint/Halasz/HalaszPoissonModes.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Counting the nonzero integer Fourier modes near a stationary point.

  1. def OAI.TwoPointCorrelations.halaszNearModes line 11
  2. lemma OAI.TwoPointCorrelations.halasz_mem_near_modes line 14
  3. lemma OAI.TwoPointCorrelations.halasz_near_modes_card line 32