OAI/Combinatorics/Progressions/Polynomial/TwistedBufferedTranslationPhase.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.bufferedTranslationTerm line 15
  2. def OAI.Erdos3.bufferedTranslationPhase line 21
  3. theorem OAI.Erdos3.bufferedTranslationTerm_nonzero_iff line 26
  4. theorem OAI.Erdos3.bufferedTranslationTerm_unique line 34
  5. theorem OAI.Erdos3.bufferedTranslationPhase_eq_chart line 44
  6. theorem OAI.Erdos3.bufferedTranslationPhase_eq_on_support line 56
  7. theorem OAI.Erdos3.bufferedTranslationPhase_norm_le_one line 64
  8. theorem OAI.Erdos3.bufferedTranslationPhase_eq_phaseFunction line 74
  9. theorem OAI.Erdos3.bufferedTranslationPhase_majorSymbol line 87
  10. theorem OAI.Erdos3.bufferedTranslationPhase_majorSymbol_on_support line 99
  11. theorem OAI.Erdos3.bufferedTranslationTerm_integer_lattice line 109
  12. theorem OAI.Erdos3.bufferedTranslationPhase_integer_lattice line 129
  13. theorem OAI.Erdos3.bufferedTranslationPhase_integerSubgroup line 142
  14. theorem OAI.Erdos3.bufferedTranslationPhase_central line 150
  15. def OAI.Erdos3.bufferedTranslationQuotientPhase line 160
  16. theorem OAI.Erdos3.bufferedTranslationQuotientPhase_mk line 168
  17. theorem OAI.Erdos3.bufferedTranslationQuotientPhase_norm_le_one line 172
  18. def OAI.Erdos3.twistedBufferedTranslationTerm line 192
  19. def OAI.Erdos3.twistedBufferedTranslationPhase line 199
  20. theorem OAI.Erdos3.twistedBufferedTranslationTerm_unique line 205
  21. theorem OAI.Erdos3.twistedBufferedTranslationPhase_eq_chart line 214
  22. theorem OAI.Erdos3.twistedBufferedTranslationTerm_norm_le_one line 228
  23. theorem OAI.Erdos3.twistedBufferedTranslationPhase_norm_le_one line 240
  24. theorem OAI.Erdos3.twistedBufferedTranslationPhase_majorSymbol line 249
  25. theorem OAI.Erdos3.twistedBufferedTranslationTerm_integer_lattice line 263
  26. theorem OAI.Erdos3.twistedBufferedTranslationPhase_integer_lattice line 287
  27. theorem OAI.Erdos3.twistedBufferedTranslationPhase_residueCover line 302
  28. theorem OAI.Erdos3.twistedBufferedTranslationTerm_central line 312
  29. theorem OAI.Erdos3.twistedBufferedTranslationPhase_central line 327
  30. def OAI.Erdos3.twistedBufferedTranslationQuotientPhase line 337
  31. theorem OAI.Erdos3.twistedBufferedTranslationQuotientPhase_mk line 346
  32. theorem OAI.Erdos3.twistedBufferedTranslationQuotientPhase_norm_le_one line 353