OAI/NumberTheory/TwoPoint/Bounds/ResidueMatrixMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reduce the actual translated matrix moment to signed closed-word expectations.

  1. theorem OAI.TwoPointCorrelations.physicalClosedPair_average_abs_le line 16
  2. theorem OAI.TwoPointCorrelations.physicalResidueMatrix_moment_le line 73