OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SourceWitnessErrorBelowTrace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.source_witness_error_below_trace line 17
2. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.source_retained_allowed_small line 41
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.retainedAllowedKernel line 66
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.retainedAllowedKernel_avg_le line 70
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.fullTraceSum line 96
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.discardedTraceSum line 100
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.fullTraceSum_le_retained_add_discarded line 105
8. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.source_full_trace_with_discarded line 128