OAI/NumberTheory/OrdinaryCorrelations/Elliott/WeightMeanOneLe.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.weightMean_one_le line 40
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.source_harmonic_upper line 46
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.sourceWindow line 57
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.sourceWindow_positive line 59
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.sourceWindow_span line 64
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.exp_linear_le_floor_power line 77
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.source_window_growth line 92
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.source_deletion_small line 125
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.moment_reserve line 169
10. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.source_divisorForm_bound line 189