OAI/NumberTheory/TwoPoint/Bounds/ActualIntervalMatrix.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual masked matrix on every sufficiently long integer interval. The error includes all initial vertices and both paths of the trace.

  1. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_interval_matrix line 16