OAI/NumberTheory/OrdinaryCorrelations/HighTrace/EdgeAt.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.edgeAt line 22
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.vertexAt line 24
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.edgeAt_step line 26
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.displacement_sum line 32
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.segment line 41
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.segment_factor_card line 46
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.segment_support line 51
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.segment_eval_factor line 61
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.segment_sum line 73
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.segment_eval line 85
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.segment_coefficient line 97
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.segment_coeff_bound line 116