OAI/NumberTheory/Ostmann/Quadratic/QuadraticSieveGrowth.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The precise exponent induction for the actual quadratic-sieve matrices

  1. def OAI.Ostmann.QuadraticSieveGrowth line 11

    Source documentation

    Heath-Brown's induction statement, with an arbitrary small-power loss.

    def QuadraticSieveGrowth (ξ : ℝ) : Prop :=
…
  2. theorem OAI.Ostmann.quadratic_sieve_growth_two line 16
  3. theorem OAI.Ostmann.quadratic_growth_shortened_transpose line 29