OAI/NumberTheory/TwoPoint/Bounds/ActualBilinearTesting.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two bounded sequences in the already-proved canonical graph estimate.

  1. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_affine_bilinear_testing line 13