OAI/NumberTheory/TwoPoint/Bounds/ActualAffineIntervalMatrix.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite-block moment on a fixed progression of origins. This allows the progression gate to be frozen before applying the trace bound.

  1. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_affine_interval_matrix_uniform line 14
  2. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_affine_interval_matrix line 124