OAI/NumberTheory/OrdinaryCorrelations/HighTrace/WitnessBaseDoublePath.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.witness_base_double_path line 20
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.witness_degree_double_path line 33
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.source_double_path_prefactor line 40
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.source_disconnected_threshold line 84