OAI/NumberTheory/Ostmann/Quadratic/CommonCenterFromTuples.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A rational common center from witnessed prime tuples

This is the finite counting step in the paragraph “One common centre for many primes” of Section 3 of the manuscript. The hypotheses are the actual family of witnessed tuples and numerical inequalities; the factorial moments and intersection estimates are proved from the congruences.

  1. def OAI.Ostmann.liftMomentUpper line 17
  2. theorem OAI.Ostmann.exists_commonCenter_of_tuple_lifts line 20