OAI/Combinatorics/Progressions/Estimates/NormalizedTwistSliceVariationPairCorrelation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.modulus_product_bound line 17
2. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_common_local_parameter_freezing line 27
3. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_common_local_parameter_cells_with_correlation line 70
4. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_untwisted_subrectangle_of_fullSliceLaw line 136
5. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_trimmed_local_parameter_cells_with_correlation line 248
6. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.trimmed_local_freezing_error_le_quarter line 310
7. theorem OAI.Erdos3.ResidueBoxSlice.fin_mean_eq_translated_zero line 336
8. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_niltest_pair_correlation_subrectangle line 357
9. theorem OAI.Erdos3.ResidueBoxSlice.fullSlicePoint_normalized_distance_le line 461
10. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_untwisted_subrectangle_of_fullSliceLaw_of_variation line 492
11. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.exists_niltest_pair_correlation_subrectangle_of_variation line 617