OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SourcePivotFactor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sourcePivotFactor line 18
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sourcePivotFactor_tendsto line 20
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sourcePivotFactor_pos line 24
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.inv_le_sourcePivotFactor line 33
5. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.source_record_parameters line 47
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.exp_return_bound line 66
7. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.source_integrated_record_sum line 73