OAI/NumberTheory/Ostmann/Construction/OriginalTwoTailContradiction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original biased tails lead to a contradiction

The Fourier and inverse-phase step produces the center used by the actual large-sieve and population argument. Only the cited published inputs remain.

  1. theorem OAI.Ostmann.eventual_original_two_tail_contradiction line 18