OAI/NumberTheory/OrdinaryCorrelations/HighTrace/AmplitudeGeOne.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.amplitude_ge_one line 19
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.occurrence_absolute_crude line 25
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.primeFactor_absolute_crude line 42
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.local_absolute_crude line 56
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.list_used_absolute_mean line 65
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.core_line_absolute_mean line 79
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.center_line_absolute_point line 96
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.center_line_absolute_mean line 125
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fullUsedIndices line 147
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.crude_prime_mean line 150
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.chronological_occurrences_le line 170
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.crude_amplitude_product line 190
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.fullUsedIndices_card_le line 204
14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.cutoffProduct_le_one line 225
15. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.absolute_list_factorization line 232
16. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.crude_unpartitioned_majorant line 241