OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/MeanR.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.SourceCircleFourier.meanC line 27
2. def OAI.OrdinaryCorrelations.SourceCircleFourier.meanR line 29
3. def OAI.OrdinaryCorrelations.SourceCircleFourier.poly line 31
4. lemma OAI.OrdinaryCorrelations.SourceCircleFourier.continuous_poly line 34
5. lemma OAI.OrdinaryCorrelations.SourceCircleFourier.mean_char line 41
6. lemma OAI.OrdinaryCorrelations.SourceCircleFourier.poly_mul line 45
7. lemma OAI.OrdinaryCorrelations.SourceCircleFourier.mean_poly line 57
8. lemma OAI.OrdinaryCorrelations.SourceCircleFourier.mean_poly_mul line 69
9. lemma OAI.OrdinaryCorrelations.SourceCircleFourier.conjugate_poly line 77
10. lemma OAI.OrdinaryCorrelations.SourceCircleFourier.meanR_cast line 83
11. lemma OAI.OrdinaryCorrelations.SourceCircleFourier.energy_real line 87
12. lemma OAI.OrdinaryCorrelations.SourceCircleFourier.fourth_moment_real line 99
13. lemma OAI.OrdinaryCorrelations.SourceCircleFourier.meanR_eq_interval line 115
14. lemma OAI.OrdinaryCorrelations.SourceCircleFourier.poly_norm_le line 121