OAI/Combinatorics/Progressions/Fourier/SiteFourierHaarMean.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finiteTensorExpansion line 12
  2. theorem OAI.Erdos3.finiteTensorCoefficientMass line 20
  3. def OAI.Erdos3.VectorPolynomial.coefficientTorusFourierSum line 37
  4. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusFourierSum_integrable line 43
  5. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusFourierSum_integral line 54
  6. def OAI.Erdos3.VectorPolynomial.dilateCoefficientFrequency line 79
  7. theorem OAI.Erdos3.VectorPolynomial.coefficientArrayFunctional_dilate line 83
  8. theorem OAI.Erdos3.VectorPolynomial.affineCoefficientModeTrivial_dilate_iff line 95
  9. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusCharacter_cover line 105
  10. theorem OAI.Erdos3.VectorPolynomial.dilateCoefficientFrequency_bound line 115
  11. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusCharacter_norm line 139
  12. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusFourierSum_norm_le line 143
  13. theorem OAI.Erdos3.VectorPolynomial.coefficientDensity_cap_of_fourier line 153
  14. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusFourierSum_mixture line 182
  15. theorem OAI.Erdos3.VectorPolynomial.coefficientFourierMixture_mass_le line 190
  16. theorem OAI.Erdos3.VectorPolynomial.coefficientFourierMixture_uniform_error line 197
  17. theorem OAI.Erdos3.VectorPolynomial.exists_coefficientFourierMixture line 208
  18. def OAI.Erdos3.VectorPolynomial.coefficientSlotFrequency line 248
  19. theorem OAI.Erdos3.VectorPolynomial.coefficientSlotFrequency_apply line 253
  20. theorem OAI.Erdos3.VectorPolynomial.coefficientSlotFrequency_bound line 259
  21. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusCharacter_slot_product line 266
  22. theorem OAI.Erdos3.VectorPolynomial.coefficientTensorFourier_eq line 286
  23. def OAI.Erdos3.VectorPolynomial.sitePullbackFrequency line 308
  24. theorem OAI.Erdos3.VectorPolynomial.sitePullbackFrequency_matrix line 313
  25. theorem OAI.Erdos3.VectorPolynomial.coefficientArrayFunctional_sitePullback line 322
  26. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusCharacter_sitePullback line 345
  27. def OAI.Erdos3.VectorPolynomial.siteTorusFourierSum line 357
  28. theorem OAI.Erdos3.VectorPolynomial.siteTorusFourierSum_pullback line 362
  29. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusFourierSum_cover line 381
  30. theorem OAI.Erdos3.VectorPolynomial.coefficientTorusFourierSum_cover_integral line 389
  31. theorem OAI.Erdos3.VectorPolynomial.siteTorusFourierSum_pullback_integrable line 412
  32. theorem OAI.Erdos3.VectorPolynomial.siteTorusFourierSum_haar_mean line 426