OAI/Combinatorics/Progressions/Fourier/NormalizedTwistLocalizedFourierSelection.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.torus_integer_character_real_phase line 11
  2. def OAI.Erdos3.VectorPolynomial.normalizedTwistFrequencyPolynomial line 32
  3. theorem OAI.Erdos3.VectorPolynomial.normalizedTwistFrequencyPolynomial_eval line 37
  4. theorem OAI.Erdos3.VectorPolynomial.normalizedTwistFrequencyPolynomial_degree line 49
  5. theorem OAI.Erdos3.VectorPolynomial.physicalGrid_character_eq_polynomial_phase line 59
  6. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_frozen_ambient_fourier line 71
  7. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.norm_correlation_star_eq_product line 113
  8. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_correlating_frequency line 127
  9. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_correlating_frequency_product line 201
  10. theorem OAI.Erdos3.VectorPolynomial.integerRowPolynomial_constant_of_annihilates line 243
  11. def OAI.Erdos3.VectorPolynomial.taggedScalarLowPolynomial line 257
  12. def OAI.Erdos3.VectorPolynomial.taggedScalarHighConstant line 260
  13. theorem OAI.Erdos3.VectorPolynomial.taggedScalar_sum_eq_low_add_constant line 263
  14. theorem OAI.Erdos3.VectorPolynomial.taggedScalarLowPolynomial_degree line 277
  15. theorem OAI.Erdos3.VectorPolynomial.taggedScalar_sum_degree line 287
  16. theorem OAI.Erdos3.VectorPolynomial.taggedScalar_sum_top line 298
  17. theorem OAI.Erdos3.VectorPolynomial.highest_nonannihilating_tag line 315
  18. def OAI.Erdos3.VectorPolynomial.truncateTaggedFrequency line 344
  19. theorem OAI.Erdos3.VectorPolynomial.integerRowPolynomial_truncateTaggedFrequency line 347
  20. theorem OAI.Erdos3.VectorPolynomial.normalizedTwistFrequencyPolynomial_truncate line 359
  21. def OAI.Erdos3.VectorPolynomial.normalizedTwistHighFrequencyConstant line 367
  22. theorem OAI.Erdos3.VectorPolynomial.normalizedTwistFrequencyPolynomial_low_degree line 372
  23. theorem OAI.Erdos3.VectorPolynomial.normalizedTwistFrequencyPolynomial_low_add_constant line 382
  24. theorem OAI.Erdos3.VectorPolynomial.normalizedTwistFrequencyPolynomial_highest_layer line 397
  25. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_correlating_frequency_early line 441
  26. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_correlating_frequency_product_early line 516
  27. theorem OAI.Erdos3.VectorPolynomial.normalizedTwistFrequencyPolynomial_top_not_approximation line 562
  28. theorem OAI.Erdos3.VectorPolynomial.normalizedTwistFrequencyPolynomial_rank_dichotomy line 589
  29. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_localized_correlating_frequency line 624