OAI/Combinatorics/Progressions/Fourier/CommonCoveredSiteCharacter.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.subspaceArrayIntegerLattice line 13
  2. abbrev OAI.Erdos3.SubspaceArrayTorus line 31
  3. theorem OAI.Erdos3.subspaceArrayFunctional_integral line 34
  4. def OAI.Erdos3.subspaceArrayCharacter line 44
  5. theorem OAI.Erdos3.subspaceArrayCharacter_mk line 50
  6. theorem OAI.Erdos3.subspaceArrayCharacter_norm line 55
  7. theorem OAI.Erdos3.subspaceArrayFunctional_mul_frequency line 69
  8. theorem OAI.Erdos3.subspaceArrayCharacter_period_multiple line 77
  9. def OAI.Erdos3.arrayCoordinateLinear line 108
  10. def OAI.Erdos3.arrayCoordinateTorus line 114
  11. theorem OAI.Erdos3.arrayCoordinateTorus_mk line 120
  12. theorem OAI.Erdos3.arrayCoordinateTorus_bijective line 124
  13. def OAI.Erdos3.arrayCoordinateEquiv line 141
  14. theorem OAI.Erdos3.arrayCoordinateEquiv_continuous line 145
  15. theorem OAI.Erdos3.integerMatrix_preserves_array_lattice line 162
  16. def OAI.Erdos3.integerMatrixTorusMap line 175
  17. theorem OAI.Erdos3.integerMatrixTorusMap_mk line 182
  18. def OAI.Erdos3.unitSubspaceCoordinate line 196
  19. def OAI.Erdos3.subspaceAmbientTorus line 202
  20. theorem OAI.Erdos3.subspaceAmbientTorus_mk line 207
  21. theorem OAI.Erdos3.subspaceAmbientTorus_continuous line 211
  22. theorem OAI.Erdos3.subspaceArrayCharacter_cover_factorization line 227
  23. def OAI.Erdos3.euclideanSubspace line 254
  24. def OAI.Erdos3.euclideanSubspaceArrayEquiv line 257
  25. theorem OAI.Erdos3.euclideanSubspaceArrayEquiv_apply line 274
  26. theorem OAI.Erdos3.euclideanSubspaceArrayEquiv_mem_lattice line 277
  27. theorem OAI.Erdos3.euclideanSubspaceArrayEquiv_map_lattice line 290
  28. def OAI.Erdos3.euclideanSubspaceTorusEquiv line 303
  29. instance OAI.Erdos3.euclideanSubspaceLattice_discrete line 310
  30. instance OAI.Erdos3.euclideanSubspaceLattice_closed line 314
  31. theorem OAI.Erdos3.euclideanSubspaceTorusEquiv_mk line 318
  32. theorem OAI.Erdos3.euclideanSubspaceTorusEquiv_continuous line 322
  33. theorem OAI.Erdos3.euclideanSubspaceTorusEquiv_symm_continuous line 326
  34. def OAI.Erdos3.euclideanSubspaceTorusHomeomorph line 331
  35. theorem OAI.Erdos3.exists_common_covered_site_character line 347