OAI/Combinatorics/Progressions/Polynomial/TranslationMajorTwistedCorrelationStepDropPolynomial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationDegreeReduced_twisted_integerEval line 15
2. theorem OAI.Erdos3.PolynomialTranslationLie.exists_reduced_majorPolynomial_degree_twisted_correlation_step_drop line 44
3. theorem OAI.Erdos3.PolynomialTranslationLie.exists_reduced_majorPolynomial_degree_twisted_correlation_potential line 142
4. theorem OAI.Erdos3.PolynomialTranslationLie.exists_reduced_majorPolynomial_degree_twisted_correlation_potential_data line 264
5. theorem OAI.Erdos3.PolynomialTranslationLie.fractionalMajor_mem_weightedSupportLE line 401
6. theorem OAI.Erdos3.PolynomialTranslationLie.majorTranslationReduced_twisted_integerEval line 408
7. theorem OAI.Erdos3.PolynomialTranslationLie.exists_reduced_majorPolynomial_twisted_correlation_step_drop line 431