Smallest denominators in intervals

DefinitionSmallest denominator in an interval#✓fully proved

For real numbers \(x\) and \(\delta\), the smallest denominator \(q_{\min}(x, \delta)\) is the least positive integer \(q\) for which there is an integer \(p\) with \(|x - p/q| < \delta/2\), that is, with \(p/q\) in the open interval \((x - \delta/2, x + \delta/2)\). If there is no such \(q\), which happens only when \(\delta \le 0\), then \(q_{\min}(x, \delta) = 0\).

noncomputable def smallestDenominator (x δ : ℝ) : ℕ :=
  sInf {q : ℕ | 0 < q ∧ ∃ p : ℤ, |x - p / q| < δ / 2}

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Equation (1.1).

Used by 7

Used byMinimality of the smallest denominator · Wide intervals have smallest denominator one · Denominators of nearby rationals bound the smallest denominator · Upper bounds on the smallest denominator · The smallest denominator is positive and attained · Convergence of the log moments of smallest denominators · Limit law of the smallest denominator

TheoremDenominators of nearby rationals bound the smallest denominator#✓fully proved

Let \(x\) and \(\delta\) be real numbers, let \(q\) be a positive integer and let \(p\) be an integer. If \(|x - p/q| < \delta/2\), then the smallest denominator satisfies \(q_{\min}(x, \delta) \le q\).

theorem smallestDenominator_le {x δ : ℝ} {q : ℕ} {p : ℤ} (hq : 0 < q)
    (hp : |x - p / q| < δ / 2) : smallestDenominator x δ ≤ q

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Equation (1.1).

Uses 1 · Used by 2

Statement usesSmallest denominator in an interval

Used byMinimality of the smallest denominator · Upper bounds on the smallest denominator

TheoremEvery real number has arbitrarily close rationals#✓fully proved

For every real number \(x\) and every real \(\delta > 0\) there are a positive integer \(q\) and an integer \(p\) with \(|x - p/q| < \delta/2\).

Taking \(q > 1/\delta\) and \(p\) the integer nearest to \(qx\) gives \(|x - p/q| \le 1/(2q) < \delta/2\).

theorem exists_denominator_mem_window (x : ℝ) {δ : ℝ} (hδ : 0 < δ) :
    ∃ q : ℕ, 0 < q ∧ ∃ p : ℤ, |x - p / q| < δ / 2

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Equation (1.1).

Used by 1

Used byThe smallest denominator is positive and attained

TheoremThe smallest denominator is positive and attained#✓fully proved

For every real number \(x\) and every real \(\delta > 0\), the smallest denominator \(q = q_{\min}(x, \delta)\) is positive and there is an integer \(p\) with \(|x - p/q| < \delta/2\).

theorem smallestDenominator_spec (x : ℝ) {δ : ℝ} (hδ : 0 < δ) :
    0 < smallestDenominator x δ ∧
      ∃ p : ℤ, |x - p / smallestDenominator x δ| < δ / 2

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Equation (1.1).

Uses 2 · Used by 1

Statement usesSmallest denominator in an interval

Proof usesEvery real number has arbitrarily close rationals

Used byUpper bounds on the smallest denominator

TheoremMinimality of the smallest denominator#✓fully proved

Let \(x\) and \(\delta\) be real numbers and let \(q\) be a positive integer with \(q < q_{\min}(x, \delta)\), where \(q_{\min}(x, \delta)\) is the smallest denominator. Then there is no integer \(p\) with \(|x - p/q| < \delta/2\).

theorem not_mem_window_of_lt_smallestDenominator {x δ : ℝ} {q : ℕ} (hq : 0 < q)
    (hlt : q < smallestDenominator x δ) (p : ℤ) : ¬ |x - p / q| < δ / 2

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Equation (1.1).

Uses 2

Statement usesSmallest denominator in an interval

Proof usesDenominators of nearby rationals bound the smallest denominator

TheoremUpper bounds on the smallest denominator#✓fully proved

Let \(x\) be a real number, let \(\delta > 0\) be real, let \(q\) be a natural number and let \(q_{\min}(x, \delta)\) be the smallest denominator. Then \(q_{\min}(x, \delta) \le q\) if and only if there are a positive integer \(q' \le q\) and an integer \(p\) with \(|x - p/q'| < \delta/2\).

theorem smallestDenominator_le_iff (x : ℝ) {δ : ℝ} (hδ : 0 < δ) (q : ℕ) :
    smallestDenominator x δ ≤ q ↔ ∃ q' ≤ q, 0 < q' ∧ ∃ p : ℤ, |x - p / q'| < δ / 2

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Equation (1.1).

Uses 3

Statement usesSmallest denominator in an interval

Proof usesDenominators of nearby rationals bound the smallest denominator · The smallest denominator is positive and attained

TheoremWide intervals have smallest denominator one#✓fully proved

For every real number \(x\) and every real \(\delta > 1\), the smallest denominator \(q_{\min}(x, \delta)\) equals \(1\).

The open interval \((x - \delta/2, x + \delta/2)\) has length greater than \(1\), so it contains an integer.

theorem smallestDenominator_eq_one {x δ : ℝ} (hδ : 1 < δ) : smallestDenominator x δ = 1

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Equation (1.1).

Uses 1

Statement usesSmallest denominator in an interval

DefinitionDensity of the logarithmic smallest denominator#✓fully proved

The function \(\eta_{\log}\) on the real line is defined by \(\eta_{\log}(s) = \frac{6}{\pi^2} e^{2s}\) for \(s \le 0\), by \(\eta_{\log}(s) = \frac{6}{\pi^2}\left(-e^{2s} + 2 + 4s\right)\) for \(0 < s \le \log 2\), and by

\[ \eta_{\log}(s) = \frac{6}{\pi^2}\left(-e^{2s} + 2 + 2e^{2s}\sqrt{\tfrac14 - e^{-2s}} - 4\log\left(\tfrac12 + \sqrt{\tfrac14 - e^{-2s}}\right)\right) \]

for \(s > \log 2\).

In the cited paper, \(\eta_{\log}\) is the density of the limit law, as \(\delta \to 0^+\), of \(\log q_{\min}(x, \delta) + \frac12 \log \delta\) for uniformly random \(x\), where \(q_{\min}(x, \delta)\) is the smallest denominator of a rational in \((x - \delta/2, x + \delta/2)\).

noncomputable def logSmallestDenominatorDensity (s : ℝ) : ℝ :=
  6 / Real.pi ^ 2 *
    if s ≤ 0 then Real.exp (2 * s)
    else if s ≤ Real.log 2 then -Real.exp (2 * s) + 2 + 4 * s
    else -Real.exp (2 * s) + 2 + 2 * Real.exp (2 * s) * Real.sqrt (1 / 4 - Real.exp (-2 * s)) -
      4 * Real.log (1 / 2 + Real.sqrt (1 / 4 - Real.exp (-2 * s)))

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Equation (1.3).

Used by 4

Used byThe log smallest-denominator density for nonpositive arguments · Value of the log smallest-denominator density at zero · Convergence of the log moments of smallest denominators · Limit law of the smallest denominator

TheoremValue of the log smallest-denominator density at zero#✓fully proved

The density \(\eta_{\log}\) of the logarithmic smallest denominator satisfies \(\eta_{\log}(0) = 6/\pi^2\).

theorem logSmallestDenominatorDensity_zero : logSmallestDenominatorDensity 0 = 6 / Real.pi ^ 2

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Equation (1.3).

Uses 1

Statement usesDensity of the logarithmic smallest denominator

TheoremThe log smallest-denominator density for nonpositive arguments#✓fully proved

For every real \(s \le 0\), the density \(\eta_{\log}\) of the logarithmic smallest denominator satisfies \(\eta_{\log}(s) = \frac{6}{\pi^2} e^{2s}\).

theorem logSmallestDenominatorDensity_of_nonpos {s : ℝ} (hs : s ≤ 0) :
    logSmallestDenominatorDensity s = 6 / Real.pi ^ 2 * Real.exp (2 * s)

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Equation (1.3).

Uses 1

Statement usesDensity of the logarithmic smallest denominator

TheoremLimit law of the smallest denominator#●ready to prove

For real \(x\) and \(\delta > 0\) let \(q_{\min}(x, \delta)\) be the smallest positive integer \(q\) such that some rational \(p/q\) lies in the open interval \((x - \delta/2, x + \delta/2)\), and let \(\eta_{\log}\) be the log smallest denominator density. Then \(\eta_{\log}\) is a probability density on \(\mathbb{R}\): \(\eta_{\log}(s) \ge 0\) for every real \(s\) and \(\int_{-\infty}^{\infty} \eta_{\log}(s) \, ds = 1\). Moreover, for all real numbers \(a\), \(b\), \(L\) with \(0 \le a \le b \le 1\), as \(\delta \to 0^+\) the Lebesgue measure of \(\{x \in [a, b] : \log q_{\min}(x, \delta) > L - \tfrac12 \log \delta\}\) tends to \((b - a) \int_L^\infty \eta_{\log}(s) \, ds\).

The interval is taken closed; its endpoints do not affect the measures.

public theorem_wanted tendsto_volume_log_smallestDenominator_gt (a b L : ℝ) (ha : 0 ≤ a)
    (hab : a ≤ b) (hb : b ≤ 1) :
    (∀ s, 0 ≤ logSmallestDenominatorDensity s) ∧ ∫ s, logSmallestDenominatorDensity s = 1 ∧
      Tendsto (fun δ => (volume {x ∈ Set.Icc a b |
          L - Real.log δ / 2 < Real.log (smallestDenominator x δ)}).toReal)
        (𝓝[>] 0) (𝓝 ((b - a) * ∫ s in Set.Ioi L, logSmallestDenominatorDensity s))

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Proposition 1.

Uses 2

Statement usesDensity of the logarithmic smallest denominator · Smallest denominator in an interval

TheoremConvergence of the log moments of smallest denominators#●ready to prove

Let \(0 \le a \le b \le 1\) be real numbers and let \(n \ge 0\) be an integer. For real \(x\) and \(\delta > 0\) let \(q_{\min}(x, \delta)\) be the smallest positive integer \(q\) such that some rational \(p/q\) lies in the open interval \((x - \delta/2, x + \delta/2)\), and let \(\eta_{\log}\) be the log smallest denominator density. Then, as \(\delta \to 0^+\),

\[ \int_a^b \bigl(\log q_{\min}(x, \delta) + \tfrac12 \log \delta\bigr)^n \, dx \to \mu_n \, (b - a), \]

where \(\mu_n = \int_{-\infty}^{\infty} s^n \, \eta_{\log}(s) \, ds\).

The moment \(\mu_n\) is an integral over the whole real line: \(\eta_{\log}\) has mass \(3/\pi^2\) on \((-\infty, 0]\), so integrating only over \(s \ge 0\) would give \(\mu_0 = 1 - 3/\pi^2\) instead of the correct limit \(1\).

public theorem_wanted tendsto_integral_log_smallestDenominator_pow (a b : ℝ) (ha : 0 ≤ a)
    (hab : a ≤ b) (hb : b ≤ 1) (n : ℕ) :
    Tendsto (fun δ => ∫ x in Set.Icc a b,
        (Real.log (smallestDenominator x δ) + Real.log δ / 2) ^ n)
      (𝓝[>] 0) (𝓝 ((∫ s, s ^ n * logSmallestDenominatorDensity s) * (b - a)))

Sources

• Jens Marklof, The Log Moments of Smallest Denominators, INTEGERS 24 (2024), Article A55, Proposition 2.

Uses 2

Statement usesDensity of the logarithmic smallest denominator · Smallest denominator in an interval

10 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.