OAI/NumberTheory/OrdinaryCorrelations/Elliott/DirMatrix.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.dirMatrix line 35
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.dirMatrix_polarization line 44
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.dirMatrix_norm_le line 75
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.dirMatrix_denominator_cancel line 87
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.retainedEdge line 113
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.retainedEdge_shift line 119
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.sum_forward_entries line 128
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.dirMatrix_bilinear_eq line 152
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Sliding.window_bilinear_le line 198