OAI/NumberTheory/OrdinaryCorrelations/HighTrace/FarCorrupted.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.farCorrupted line 23
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.short_far_corrupted_card line 26
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.farCorrupted_walk_long line 33
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.farCorruptSum line 46
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.corrupted_near_far_of_threshold line 53
6. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.source_full_trace_near_far line 84