OAI/Combinatorics/Progressions/Linear/ExternalFamilyCircleProjection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.norm_weighted_mean_sub_le line 12
2. theorem OAI.Erdos3.finite_projection_tested_error line 23
3. theorem OAI.Erdos3.norm_finiteWeightedSum_sub_le line 82
4. theorem OAI.Erdos3.finiteWeightedProjection_error line 98
5. theorem OAI.Erdos3.CircleFourier.lipschitz_finite_complex_sum line 156
6. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_tested_error line 170
7. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_tested_difference_le line 217
8. theorem OAI.Erdos3.FiniteProbabilityWeights.finite_projection_tested_error line 225
9. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_tested_weighted_error line 280
10. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_weighted_error line 314
11. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_family_tested_weighted_error line 396