OAI/Combinatorics/Progressions/Fourier/PlateauFourierMode.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.realLinearCharacter line 15
  2. theorem OAI.Erdos3.realLinearCharacter_norm line 18
  3. theorem OAI.Erdos3.realLinearCharacter_lipschitz line 21
  4. def OAI.Erdos3.plateauFourierMode line 49
  5. theorem OAI.Erdos3.plateauFourierMode_norm line 52
  6. theorem OAI.Erdos3.plateauFourierMode_lipschitz line 57
  7. def OAI.Erdos3.rationalGridPhase line 77
  8. theorem OAI.Erdos3.rationalGridPhase_norm line 80
  9. theorem OAI.Erdos3.rationalGridPhase_intCast line 83
  10. theorem OAI.Erdos3.plateau_grid_character_split line 96