Baker–Davenport reduction

TheoremNearest-integer estimate in the Baker–Davenport reduction#✓fully proved

For a real number \(x\) write \(\lVert x \rVert = |x - \operatorname{round}(x)|\) for the distance from \(x\) to a nearest integer. Let \(q\), \(M\), \(u\) be natural numbers with \(u \le M\), let \(v\) be an integer, and let \(\kappa\) and \(\mu\) be real numbers. If \(\varepsilon = \lVert \mu q \rVert - M \lVert \kappa q \rVert\), then \(\varepsilon \le q \, |u\kappa - v + \mu|\).

theorem nearestInteger_reduction_core (q M u : ℕ) (kappa mu : ℝ) (v : ℤ)
    (hu : u ≤ M)
    (epsilon : ℝ)
    (heq : epsilon = |mu * (q : ℝ) - (round (mu * (q : ℝ)) : ℝ)| -
      (M : ℝ) * |kappa * (q : ℝ) - (round (kappa * (q : ℝ)) : ℝ)|) :
    epsilon ≤ (q : ℝ) * |(u : ℝ) * kappa - (v : ℝ) + mu|
Sources
  • Nearest-integer Baker–Davenport reduction core: a named reusable arithmetic prerequisite stage extracted from Lemma (lines 285--292) of Eric F. Bravo, Carlos A. Gómez, and Florian Luca, "Product of Consecutive Tribonacci Numbers With Only One Distinct Digit", Journal of Integer Sequences 22 (2019), Article 19.6.3. https://cs.uwaterloo.ca/journals/JIS/VOL22/Gomez/gomez3.tex. Scope: the printed lemma defines nearest-integer distance by ‖x‖ = |x - round x| and ε := ‖μq‖ - M‖κq‖; this stage records the reverse-triangle inequality used by the reduction argument. It does not claim to formalize the full lemma. The source's irrationality, continued-fraction, q > 6M, and logarithmic hypotheses belong to the later wrapper and are deliberately omitted from this arithmetic stage, as are the source's 0 < q and 0 < ε, which the inequality does not need. The explicit heq equality hypothesis is necessary: a prior default-valued epsilon binder did not assert the definition and made the statement false.
Used by 1
Used byBaker–Davenport reduction for an arbitrary denominator, absolute-value form

TheoremBaker–Davenport reduction for an arbitrary denominator, absolute-value form#✓fully proved

For a real number \(x\) write \(\lVert x \rVert = |x - \operatorname{round}(x)|\) for the distance from \(x\) to a nearest integer. Let \(M\) and \(q\) be natural numbers with \(q > 0\), and let \(\kappa\), \(\mu\), \(A\), \(B\) be real numbers with \(A > 0\) and \(B > 1\). Put \(\varepsilon = \lVert \mu q \rVert - M \lVert \kappa q \rVert\) and suppose that \(\varepsilon > 0\). Then there are no natural numbers \(r\), \(s\), \(w\) with \(r \le M\), \(w \ge \log(Aq/\varepsilon) / \log B\) and \(|r\kappa - s + \mu| < A B^{-w}\).

theorem bakerDavenport_reduction_absolute_general
    (M q : ℕ) (hq : 0 < q)
    (kappa A mu B epsilon : ℝ)
    (hA : 0 < A) (hB : 1 < B)
    (hepsilon : epsilon = |mu * (q : ℝ) - (round (mu * (q : ℝ)) : ℝ)| -
      (M : ℝ) * |kappa * (q : ℝ) - (round (kappa * (q : ℝ)) : ℝ)|)
    (hepsilonpos : 0 < epsilon) :
    ¬∃ (r s w : ℕ), r ≤ M ∧
      (w : ℝ) ≥ Real.log (A * (q : ℝ) / epsilon) / Real.log B ∧
      |(r : ℝ) * kappa - (s : ℝ) + mu| < A * (B⁻¹) ^ w
Uses 1 · Used by 1
Proof usesNearest-integer estimate in the Baker–Davenport reduction
Used byBaker–Davenport reduction lemma, absolute-value form

TheoremBaker–Davenport reduction lemma, absolute-value form#✓fully proved

For a real number \(x\) write \(\lVert x \rVert = |x - \operatorname{round}(x)|\) for the distance from \(x\) to a nearest integer. Let \(M\) be a positive integer and \(\kappa\) an irrational real number, and let \(q\) be the denominator of the \(j\)-th convergent of the continued fraction of \(\kappa\) for some natural number \(j\), with \(q > 6M\). Let \(A\), \(B\), \(\mu\) be real numbers with \(A > 0\) and \(B > 1\). Put \(\varepsilon = \lVert \mu q \rVert - M \lVert \kappa q \rVert\) and suppose that \(\varepsilon > 0\). Then there are no positive integers \(r\), \(s\), \(w\) with \(r \le M\), \(w \ge \log(Aq/\varepsilon) / \log B\) and \(0 < |r\kappa - s + \mu| < A B^{-w}\).

Of the hypothesis \(q > 6M\) only \(q > 0\) is used. The hypotheses that \(M > 0\), that \(\kappa\) is irrational and that \(q\) is a convergent denominator, and the positivity of \(r\), \(s\), \(w\) and of \(|r\kappa - s + \mu|\), are not needed: the statement follows from the version for an arbitrary positive denominator.

MetaMathlibExt.bakerDavenport_reduction_absolute · 15 lines 
theorem bakerDavenport_reduction_absolute
    (M : ℕ) (hM : 0 < M)
    (kappa : ℝ) (hkappa : Irrational kappa)
    (j : ℕ) (q : ℕ)
    (hq : q = (kappa.convergent j).den)
    (hqM : 6 * M < q)
    (A mu B epsilon : ℝ)
    (hA : 0 < A) (hB : 1 < B)
    (hepsilon : epsilon = |mu * (q : ℝ) - (round (mu * (q : ℝ)) : ℝ)| -
      (M : ℝ) * |kappa * (q : ℝ) - (round (kappa * (q : ℝ)) : ℝ)|)
    (hepsilonpos : 0 < epsilon) :
    ¬∃ (r s w : ℕ), 0 < r ∧ 0 < s ∧ 0 < w ∧ r ≤ M ∧
      (w : ℝ) ≥ Real.log (A * (q : ℝ) / epsilon) / Real.log B ∧
      0 < |(r : ℝ) * kappa - (s : ℝ) + mu| ∧
      |(r : ℝ) * kappa - (s : ℝ) + mu| < A * (B⁻¹) ^ w
Sources
Uses 1
Proof usesBaker–Davenport reduction for an arbitrary denominator, absolute-value form

TheoremBaker–Davenport reduction for an arbitrary denominator, one-sided form#✓fully proved

For a real number \(x\) write \(\lVert x \rVert = |x - \operatorname{round}(x)|\) for the distance from \(x\) to a nearest integer. Let \(N\) and \(q\) be natural numbers with \(q > 0\), and let \(\gamma\), \(\mu\), \(A\), \(B\) be real numbers with \(A > 0\) and \(B > 1\). Put \(\xi = \lVert \mu q \rVert - N \lVert \gamma q \rVert\) and suppose that \(\xi > 0\). Then there are no natural numbers \(u\), \(v\), \(w\) with \(u \le N\), \(w \ge \log(Aq/\xi) / \log B\) and \(0 < u\gamma - v + \mu < A B^{-w}\).

theorem bakerDavenport_reduction_oneSided_general
    (N q : ℕ) (hq : 0 < q)
    (γ A μ B ξ : ℝ)
    (hA : 0 < A) (hB : 1 < B)
    (hξ : ξ = |μ * (q : ℝ) - (round (μ * (q : ℝ)) : ℝ)| -
      (N : ℝ) * |γ * (q : ℝ) - (round (γ * (q : ℝ)) : ℝ)|)
    (hξpos : 0 < ξ) :
    ¬∃ (u v w : ℕ), u ≤ N ∧
      (w : ℝ) ≥ Real.log (A * (q : ℝ) / ξ) / Real.log B ∧
      0 < (u : ℝ) * γ - (v : ℝ) + μ ∧
      (u : ℝ) * γ - (v : ℝ) + μ < A * (B⁻¹) ^ w
Used by 1
Used byBaker–Davenport reduction lemma, one-sided form

TheoremBaker–Davenport reduction lemma, one-sided form#✓fully proved

For a real number \(x\) write \(\lVert x \rVert = |x - \operatorname{round}(x)|\) for the distance from \(x\) to a nearest integer. Let \(N\) be a positive integer and \(\gamma\) an irrational real number, and let \(q\) be the denominator of the \(j\)-th convergent of the continued fraction of \(\gamma\) for some natural number \(j\), with \(q > 6N\). Let \(A\), \(B\), \(\mu\) be real numbers with \(A > 0\) and \(B > 1\). Put \(\xi = \lVert \mu q \rVert - N \lVert \gamma q \rVert\) and suppose that \(\xi > 0\). Then there are no positive integers \(u\), \(v\), \(w\) with \(u \le N\), \(w \ge \log(Aq/\xi) / \log B\) and \(0 < u\gamma - v + \mu < A B^{-w}\).

Of the hypothesis \(q > 6N\) only \(q > 0\) is used. The hypotheses that \(N > 0\), that \(\gamma\) is irrational and that \(q\) is a convergent denominator, and the positivity of \(u\), \(v\) and \(w\), are not needed: the statement follows from the version for an arbitrary positive denominator.

MetaMathlibExt.bakerDavenport_reduction_oneSided · 15 lines 
theorem bakerDavenport_reduction_oneSided
    (N : ℕ) (hN : 0 < N)
    (γ : ℝ) (hγ : Irrational γ)
    (j : ℕ) (q : ℕ)
    (hq : q = (γ.convergent j).den)
    (hqN : 6 * N < q)
    (A μ B ξ : ℝ)
    (hA : 0 < A) (hB : 1 < B)
    (hξ : ξ = |μ * (q : ℝ) - (round (μ * (q : ℝ)) : ℝ)| -
      (N : ℝ) * |γ * (q : ℝ) - (round (γ * (q : ℝ)) : ℝ)|)
    (hξpos : 0 < ξ) :
    ¬∃ (u v w : ℕ), 0 < u ∧ 0 < v ∧ 0 < w ∧ u ≤ N ∧
      (w : ℝ) ≥ Real.log (A * (q : ℝ) / ξ) / Real.log B ∧
      0 < (u : ℝ) * γ - (v : ℝ) + μ ∧
      (u : ℝ) * γ - (v : ℝ) + μ < A * (B⁻¹) ^ w
Sources
Uses 1
Proof usesBaker–Davenport reduction for an arbitrary denominator, one-sided form
5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.