OAI/NumberTheory/Ostmann/Quadratic/CommonCenterLiftBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeTupleProduct line 12
2. theorem OAI.Ostmann.primeTupleProduct_pos line 14
3. theorem OAI.Ostmann.tuple_prime_coprime line 18
4. theorem OAI.Ostmann.tuple_lifts_modEq line 29

   Source documentation

   Two lifts of the same distinct prime tuple lie in the same progression modulo the product of those primes.

   theorem tuple_lifts_modEq (P : Finset ℕ) (hprime : ∀ p ∈ P, p.Prime)
       (a : ℤ) (t : ℕ → ℤ) {r : ℕ} (e : Fin r ↪ P) (n m : ℤ)
       (hn : ∀ i, ((e i).1 : ℤ) ∣ n - a * t (e i).1)
       (hm : ∀ i, ((e i).1 : ℤ) ∣ m - a * t (e i).1) :
       n ≡ m [ZMOD (primeTupleProduct P e : ℤ)] := by
   …

   Mentions: OAI.Ostmann.primeTupleProduct

5. def OAI.Ostmann.integerLiftSet line 46
6. theorem OAI.Ostmann.card_integerLiftSet_le line 52

   Source documentation

   Uniform in the chosen tuple and its residue class.

   theorem card_integerLiftSet_le (P : Finset ℕ) (hprime : ∀ p ∈ P, p.Prime)
       (a : ℤ) (t : ℕ → ℤ) {r : ℕ} (e : Fin r ↪ P) (H : ℕ) :
       ((integerLiftSet P a t e H).card : ℚ) ≤
         (2 * (H : ℚ) + 1) / (primeTupleProduct P e : ℚ) + 1 := by
   …

   Mentions: OAI.Ostmann.integerLiftSet, OAI.Ostmann.primeTupleProduct

7. theorem OAI.Ostmann.primeTupleProduct_lower line 80
8. theorem OAI.Ostmann.card_integerLiftSet_le_uniform line 87

   Source documentation

   The bound used in the lower factorial moment is uniform over the tuple.

   theorem card_integerLiftSet_le_uniform (P : Finset ℕ) (hprime : ∀ p ∈ P, p.Prime)
       (a : ℤ) (t : ℕ → ℤ) {r : ℕ} (e : Fin r ↪ P) (H Z : ℕ)
       (hZ : 0 < Z) (hmin : ∀ p ∈ P, Z ≤ p) :
       ((integerLiftSet P a t e H).card : ℚ) ≤ (2 * (H : ℚ) + 1) / (Z : ℚ) ^ r + 1 := by
   …

   Mentions: OAI.Ostmann.integerLiftSet