OAI/NumberTheory/TwoPoint/Walks/RetainedComplexMatrix.lean
3 declarations, 0 contain sorry, 0 declared as axioms
The exact symmetric retained matrix for arbitrary complex tests.
- lemma
OAI.TwoPointCorrelations.retainedRealEdge_reverse_testline 13 - def
OAI.TwoPointCorrelations.retainedDirectedMatrixline 31 - theorem
OAI.TwoPointCorrelations.retained_matrix_bilinearline 39