OAI/NumberTheory/Ostmann/QuadraticCenter/RationalApproximationLift.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.approximationLift line 10
2. theorem OAI.Ostmann.approximationLift_congruence line 12
3. theorem OAI.Ostmann.approximationLift_abs_bound line 24
4. theorem OAI.Ostmann.approximationLift_tuple line 38

   Source documentation

   The rational approximation supplies exactly the bounded integer and the simultaneous congruences used by the lift-moment argument.

   theorem approximationLift_tuple (P : Finset ℕ) (hprime : ∀ p ∈ P, p.Prime)
       {k : ℕ} (e : Fin k ↪ P) (a H : ℕ) (tM b : ℤ) (t : ℕ → ℤ)
       (δ : ℝ)
       (happrox : |(a : ℝ) * ((tM : ℝ) / primeTupleProduct P e) - b| ≤ δ)
       (hsize : (primeTupleProduct P e : ℝ) * δ ≤ H)
       (ht : ∀ i, ((e i).1 : ℤ) ∣ tM - t (e i).1) :
       ∃ n ∈ Finset.Ico (-(H : ℤ)) (H + 1),
         ∀ i, ((e i).1 : ℤ) ∣ n - (a : ℤ) * t (e i).1 := by
   …

   Mentions: OAI.Ostmann.primeTupleProduct