OAI/Combinatorics/Progressions/Estimates/LocalAverageAmplitude.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.finite_weighted_test_summable line 12
2. theorem OAI.Erdos3.finite_weighted_test_norm_le line 18
3. theorem OAI.Erdos3.finite_weighted_translation_test_le line 28
4. theorem OAI.Erdos3.normalized_finite_translation_test_le line 51
5. theorem OAI.Erdos3.finite_weighted_expect_comm line 70
6. theorem OAI.Erdos3.finite_probability_test_norm_le line 83
7. theorem OAI.Erdos3.finite_probability_shift_transfer line 96
8. theorem OAI.Erdos3.norm_local_average_amplitude_le line 131