OAI/NumberTheory/Ostmann/QuadraticCenter/UniformDenominatorLifts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.exists_uniform_denominator_lifts line 12
2. theorem OAI.Ostmann.exists_commonCenter_of_bounded_denominators line 49

   Source documentation

   The common-center theorem applies to tuple-dependent denominators: the finite pigeonhole loss is paid explicitly before the moment argument.

   theorem exists_commonCenter_of_bounded_denominators (P : Finset ℕ)
       (t : ℕ → ℤ) (k d K H Z Amax : ℕ) (hd : d ≤ k + 1)
       (A V : ℝ) (hA : 0 < A) (hV : 0 < V) (hZ : 0 < Z) (hAmax : 0 < Amax)
       (hprime : ∀ p ∈ P, p.Prime) (hap : ∀ p ∈ P, Amax < p)
       (hmin : ∀ p ∈ P, Z ≤ p) (hlog : ∀ p ∈ P, V ≤ Real.log (p : ℝ))
       (hbudget : Real.log (2 * (H : ℝ)) < (K + 1 : ℕ) * V)
       (hsmall : 2 * K * (P.card : ℝ) ≤ A ^ 2)
       (E : Finset (Fin (k + 1) ↪ P))
       (hlift : ∀ e ∈ E, ∃ a ∈ Finset.Icc 1 Amax,
         ∃ n ∈ Finset.Ico (-(H : ℤ)) (H + 1),
           ∀ i, ((e i).1 : ℤ) ∣ n - (a : ℤ) * t (e i).1)
       (hpositive : 0 < (E.card : ℝ) / Amax -
   …