OAI/NumberTheory/TwoPoint/Bounds/ActualMatrixTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual residue-model matrix moment at the canonical trace length.

  1. theorem OAI.TwoPointCorrelations.eventually_actual_matrix_trace line 12