OAI/NumberTheory/OrdinaryCorrelations/HighTrace/UsedPrimeReciprocal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.usedPrimeReciprocal line 17
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.usedPrimeReciprocal_nonneg line 20
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.traceIntegrationMajorant line 25
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.traceIntegrationMajorant_nonneg line 32
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.traceIntegrationMajorant_mono line 39
6. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.trace_integration_finite line 50
7. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.trace_integration_source line 76
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.assignedKernelIntegral_mono line 97
9. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.trace_integration_retained line 110
10. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.source_active_graph_eventually line 119