OAI/Combinatorics/Progressions/Fourier/EuclideanJetTorus.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.coefficientIntegerLattice line 13
  2. abbrev OAI.Erdos3.VectorPolynomial.CoefficientTorus line 31
  3. theorem OAI.Erdos3.VectorPolynomial.coefficientArrayFunctional_integral line 35
  4. def OAI.Erdos3.VectorPolynomial.coefficientTorusCharacter line 46
  5. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusCharacter_mk line 53
  6. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusCharacter_integrable line 60
  7. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusCharacter_integral line 70
  8. abbrev OAI.Erdos3.VectorPolynomial.CoefficientCoordinateTori line 89
  9. def OAI.Erdos3.VectorPolynomial.coefficientCoordinateArray line 93
  10. def OAI.Erdos3.VectorPolynomial.coefficientCoordinateTorus line 100
  11. theorem OAI.Erdos3.VectorPolynomial.coefficientCoordinateTorus_mk line 107
  12. theorem OAI.Erdos3.VectorPolynomial.coefficientCoordinateTorus_surjective line 113
  13. theorem OAI.Erdos3.VectorPolynomial.coefficientCoordinateTorus_continuous line 125
  14. theorem OAI.Erdos3.VectorPolynomial.coefficientCoordinateTori_compact line 133
  15. def OAI.Erdos3.VectorPolynomial.coefficientLayerArray line 149
  16. theorem OAI.Erdos3.VectorPolynomial.coefficientLayerArray_preserves_lattice line 156
  17. def OAI.Erdos3.VectorPolynomial.coefficientLayerTorus line 162
  18. theorem OAI.Erdos3.VectorPolynomial.coefficientLayerTorus_mk line 170
  19. theorem OAI.Erdos3.VectorPolynomial.coefficientLayerTorus_continuous line 176
  20. instance OAI.Erdos3.VectorPolynomial.coefficientIntegerLattice_closed line 193
  21. theorem OAI.Erdos3.VectorPolynomial.coefficientTorus_compact_of_basis line 212
  22. def OAI.Erdos3.VectorPolynomial.coefficientTorusHaar line 229
  23. instance OAI.Erdos3.VectorPolynomial.coefficientTorusHaar_probability line 239
  24. instance OAI.Erdos3.VectorPolynomial.coefficientTorusHaar_invariant line 250
  25. def OAI.Erdos3.VectorPolynomial.affineSampleCoefficientArray line 271
  26. theorem OAI.Erdos3.VectorPolynomial.affineSampleCoefficientArray_val line 278
  27. theorem OAI.Erdos3.VectorPolynomial.coefficientArrayFunctional_sample line 287
  28. def OAI.Erdos3.VectorPolynomial.affineSampleCoefficientTorus line 304
  29. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusCharacter_sample line 310
  30. theorem OAI.Erdos3.integerMatrixTorusMap_continuous line 329
  31. abbrev OAI.Erdos3.VectorPolynomial.SiteTorus line 338
  32. def OAI.Erdos3.VectorPolynomial.coefficientSiteTorusMap line 341
  33. theorem OAI.Erdos3.VectorPolynomial.coefficientSiteTorusMap_mk line 347
  34. theorem OAI.Erdos3.VectorPolynomial.coefficientSiteTorusMap_continuous line 355
  35. def OAI.Erdos3.VectorPolynomial.zeroCoefficientExponent line 373
  36. def OAI.Erdos3.VectorPolynomial.constantCoefficientTorus line 376
  37. theorem OAI.Erdos3.VectorPolynomial.constantCoefficientTorus_mk line 380
  38. theorem OAI.Erdos3.VectorPolynomial.constantCoefficientTorus_continuous line 391
  39. theorem OAI.Erdos3.VectorPolynomial.oneSite_constantCoefficientTorus line 395
  40. theorem OAI.Erdos3.VectorPolynomial.oneSite_add_constantCoefficientTorus line 408
  41. theorem OAI.Erdos3.matrixModuleAction_surjective_of_period line 426
  42. theorem OAI.Erdos3.integerMatrixTorusMap_surjective_of_period line 460
  43. theorem OAI.Erdos3.integerMatrixTorusMap_comp line 471
  44. abbrev OAI.Erdos3.VectorPolynomial.BooleanJetTorus line 497
  45. def OAI.Erdos3.VectorPolynomial.siteBooleanJetTorusMap line 500
  46. theorem OAI.Erdos3.VectorPolynomial.siteBooleanJetTorusMap_continuous line 507
  47. def OAI.Erdos3.VectorPolynomial.coefficientBooleanJetTorusMap line 513
  48. theorem OAI.Erdos3.VectorPolynomial.coefficientBooleanJetTorusMap_mk line 519
  49. theorem OAI.Erdos3.VectorPolynomial.coefficientBooleanJetTorusMap_continuous line 535
  50. theorem OAI.Erdos3.VectorPolynomial.coefficientBooleanJetTorusMap_surjective line 543
  51. abbrev OAI.Erdos3.VectorPolynomial.EuclideanJetLayers line 576
  52. instance OAI.Erdos3.VectorPolynomial.euclideanJetLayers_borel line 580
  53. def OAI.Erdos3.VectorPolynomial.euclideanJetEquiv line 589
  54. theorem OAI.Erdos3.VectorPolynomial.euclideanJetEquiv_continuous line 607