OAI/NumberTheory/TwoPoint/Walks/ColumnMatrixTrace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual residue-model matrix is bounded by the same literal column catalog to which the four trace estimates apply.

  1. def OAI.TwoPointCorrelations.actualColumnLabel line 14
  2. theorem OAI.TwoPointCorrelations.columnMatrix_residue_trace_le line 19