OAI/NumberTheory/Ostmann/Construction/TupleFrequencyCutoff.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual finite frequency support of the initial tuple amplitude

  1. def OAI.Ostmann.tupleFrequencies line 11
  2. theorem OAI.Ostmann.tupleGraphPhase_zero_at_zero line 15
  3. theorem OAI.Ostmann.fourier_zero_beyond_tuple_cutoff line 24
  4. theorem OAI.Ostmann.tupleFrequencyTerm_zero line 42
  5. theorem OAI.Ostmann.tuple_character_poisson_finite line 62