OAI/Combinatorics/Progressions/Fourier/NormalizedTwistSingleSiteFourierHaar.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.ambientIntegerCharacter line 13
  2. theorem OAI.Erdos3.ambientIntegerCharacter_norm line 17
  3. theorem OAI.Erdos3.ambientIntegerCharacter_lipschitz line 22
  4. theorem OAI.Erdos3.ambientIntegerCharacter_reconstruction line 44
  5. def OAI.Erdos3.ambientFourierSum line 61
  6. theorem OAI.Erdos3.ambientFourierSum_norm_le line 65
  7. theorem OAI.Erdos3.ambientFourierSum_lipschitz line 72
  8. def OAI.Erdos3.VectorPolynomial.coefficientFourierAmbient line 113
  9. theorem OAI.Erdos3.VectorPolynomial.coefficientFourierAmbient_eq line 116
  10. theorem OAI.Erdos3.VectorPolynomial.coefficientFourierAmbient_norm_le line 128
  11. theorem OAI.Erdos3.VectorPolynomial.coefficientFourierAmbient_lipschitz line 133
  12. theorem OAI.Erdos3.VectorPolynomial.exists_mean_coefficient_ambient_approximation line 140
  13. def OAI.Erdos3.VectorPolynomial.booleanSiteAmbientFrequency line 178
  14. theorem OAI.Erdos3.VectorPolynomial.booleanSiteAmbientFrequency_bound line 184
  15. theorem OAI.Erdos3.VectorPolynomial.ambientJetCharacter_site_factorization line 201
  16. def OAI.Erdos3.VectorPolynomial.booleanCharacterSiteFactor line 250
  17. theorem OAI.Erdos3.VectorPolynomial.booleanCharacterSiteFactor_norm line 256
  18. theorem OAI.Erdos3.VectorPolynomial.booleanCharacterSiteFactor_lipschitz line 263
  19. theorem OAI.Erdos3.VectorPolynomial.booleanCharacterSiteFactor_product line 283
  20. theorem OAI.Erdos3.VectorPolynomial.booleanCharacterSiteFactor_expansion line 294
  21. def OAI.Erdos3.VectorPolynomial.singleSiteEuclideanRow line 319
  22. theorem OAI.Erdos3.VectorPolynomial.singleSiteEuclideanRow_apply line 324
  23. theorem OAI.Erdos3.VectorPolynomial.singleSiteEuclideanRow_integral line 330
  24. theorem OAI.Erdos3.VectorPolynomial.singleSiteEuclideanRow_eq_zero line 342
  25. theorem OAI.Erdos3.VectorPolynomial.singleSiteEuclideanRow_character line 358
  26. theorem OAI.Erdos3.VectorPolynomial.singleSiteHaar_ambientIntegerCharacter_integral line 374
  27. theorem OAI.Erdos3.VectorPolynomial.singleSiteHaar_ambientIntegerCharacter_integrable line 411