OAI/Combinatorics/Progressions/Fourier/MajorPhaseLowFourierExtraction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_majorPhaseLowFourierExtraction_budget line 12
2. theorem OAI.Erdos3.VectorPolynomial.normalizedTwistFrequencyPolynomial_truncate_correlation line 42
3. theorem OAI.Erdos3.VectorPolynomial.exists_normalizedTwist_high_frequency_removal_on_progression line 79
4. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_rank_localized_correlating_frequency line 180
5. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_low_localized_correlating_frequency line 280
6. theorem OAI.Erdos3.VectorPolynomial.normalizedTwistFrequencyPolynomial_eq_zero_of_annihilates line 352
7. theorem OAI.Erdos3.VectorPolynomial.exists_normalizedTwist_uniform_box_frequency_comparison line 365
8. theorem OAI.Erdos3.VectorPolynomial.exists_normalizedTwist_uniform_box_fourier_comparison line 418
9. def OAI.Erdos3.VectorPolynomial.majorPhaseSample line 471
10. theorem OAI.Erdos3.VectorPolynomial.exists_majorPhase_low_localized_correlating_frequency line 483