OAI/NumberTheory/Ostmann/QuadraticCenter/RationalPhaseSeparation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.exists_reduced_phase_approximation line 13

   Source documentation

   Dirichlet approximation in exactly the form needed by quadratic Weyl differencing; the numerator and denominator are reduced.

   theorem exists_reduced_phase_approximation (θ : ℝ) (Q : ℕ) (hQ : 0 < Q) :
       ∃ (a : ℤ) (r : ℕ), 0 < r ∧ r ≤ Q ∧ a.natAbs.Coprime r ∧
         |θ - (a : ℝ) / r| ≤ 1 / (((Q : ℝ) + 1) * r) ∧
         |θ - (a : ℝ) / r| ≤ 1 / (r : ℝ) ^ 2 := by
   …

2. theorem OAI.Ostmann.rational_phase_shift_separation line 30

   Source documentation

   A nonzero short shift cannot be too close to any integer. This is the separation claim used inside each block of length at most r/2.

   theorem rational_phase_shift_separation (θ : ℝ) (a δ k : ℤ) (r : ℕ)
       (hr : 0 < r) (hcop : a.natAbs.Coprime r) (hδ : δ ≠ 0)
       (hshort : 2 * |(δ : ℝ)| ≤ r)
       (happrox : |θ - (a : ℝ) / r| ≤ 1 / (r : ℝ) ^ 2) :
       1 / (2 * (r : ℝ)) ≤ |(δ : ℝ) * θ - k| := by
   …