OAI/NumberTheory/OrdinaryCorrelations/Elliott/NormThreshold.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.norm_threshold line 38
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.windowWeight line 56
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.windowSquare line 59
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.windowWeight_nonneg line 62
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.windowSquare_nonneg line 64
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.windowWeight_sq_le line 67
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.windowWeight_mean line 74
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.windowSquare_mean line 80
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.weighted_norm_average_le line 87
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.weighted_norm_eventual line 129