OAI/NumberTheory/TwoPoint/Bounds/ActualAffineSpectralTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exceptional origins along a fixed progression for the actual finite block.

  1. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_affine_spectral_tail_uniform line 13
  2. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_affine_spectral_tail line 71