OAI/Combinatorics/Progressions/Linear/CircleFejerKernel.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.CircleFourier.fejerPairFrequency line 14
2. def OAI.Erdos3.CircleFourier.fejerFrequencies line 17
3. def OAI.Erdos3.CircleFourier.fejerCoefficient line 21
4. def OAI.Erdos3.CircleFourier.fejerPolynomial line 26
5. lemma OAI.Erdos3.CircleFourier.fejer_grouped line 30
6. lemma OAI.Erdos3.CircleFourier.fejer_pair_sum_eq line 42
7. lemma OAI.Erdos3.CircleFourier.fejer_neg_sum_eq_conj line 62
8. lemma OAI.Erdos3.CircleFourier.fejer_fin_sum_eq_geo line 75
9. lemma OAI.Erdos3.CircleFourier.fejer_pair_sum_eq_norm_sq line 83
10. lemma OAI.Erdos3.CircleFourier.complex_fejerPolynomial_eq line 93
11. lemma OAI.Erdos3.CircleFourier.fejerPolynomial_eq line 119
12. lemma OAI.Erdos3.CircleFourier.fejerPolynomial_nonneg line 124
13. lemma OAI.Erdos3.CircleFourier.fejerPolynomial_le_of_distance line 129
14. lemma OAI.Erdos3.CircleFourier.integral_character line 149
15. lemma OAI.Erdos3.CircleFourier.integral_fejerPolynomial line 158
16. lemma OAI.Erdos3.CircleFourier.fejer_fiber_card_le line 226
17. lemma OAI.Erdos3.CircleFourier.fejerCoefficient_nonneg line 244
18. lemma OAI.Erdos3.CircleFourier.fejerCoefficient_le_one line 249
19. lemma OAI.Erdos3.CircleFourier.continuous_fejerPolynomial line 255
20. lemma OAI.Erdos3.CircleFourier.norm_geometricCharacterSum_le_card line 270
21. lemma OAI.Erdos3.CircleFourier.fejerPolynomial_le_card line 278
22. lemma OAI.Erdos3.CircleFourier.integrable_fejerPolynomial_comp_sub line 287
23. lemma OAI.Erdos3.CircleFourier.fejerPolynomial_neg line 297
24. lemma OAI.Erdos3.CircleFourier.integral_fejerPolynomial_comp_sub line 314