OAI/NumberTheory/OrdinaryCorrelations/Elliott/Adj.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.Adj line 45
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.adj_ne line 48
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.WindowWalk line 56
4. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.(instance at line 60) line 60
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.WindowWalk.label line 66
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.WindowWalk.label_mem line 68
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.WindowWalk.label_step line 70
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.WindowWalk.sign line 75
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.WindowWalk.line line 78
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.WindowWalk.encode_injective line 102
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.integer_vertex_shift line 118
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.integer_edge_shift line 127
13. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.edgeCoeff line 142
14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.edgeCoeff_zero line 146
15. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.label_unique line 154
16. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.edgeCoeff_eq line 166
17. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.symMatrix line 188
18. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.symMatrix_zero line 199
19. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.symMatrix_entry line 211
20. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.symMatrix_hermitian line 233
21. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.walk_allowed_iff line 264
22. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.WindowWalk.coefficient line 278
23. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.WindowWalk.coefficient_norm line 282
24. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.WindowWalk.matrix_product line 289
25. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.matrix_trace line 326
26. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.matrix_norm_moment line 354