OAI/Combinatorics/Progressions/Fourier/ProductFrequencyKernel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.piFrequency line 15
  2. theorem OAI.Erdos3.piFrequency_apply line 18
  3. theorem OAI.Erdos3.piFrequency_single line 23
  4. theorem OAI.Erdos3.realify_piFrequency line 33
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.piFrequency_basis line 46
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.piFrequency_logHeight line 57
  7. theorem OAI.Erdos3.realify_piFrequency_eq_component line 78
  8. theorem OAI.Erdos3.realify_component_zero_of_piFrequency_zero line 89