OAI/NumberTheory/TwoPoint/Bounds/ActualAffineTesting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Average the actual graph test over fixed-progression block origins, using compression on good blocks and the deterministic bound elsewhere.

  1. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_affine_testing_uniform line 14
  2. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_affine_testing line 108