Duffin–Schaeffer conjecture

DefinitionThe approximation inequality (1.7)#✓fully proved

For a function \(\psi\) from the positive integers to the nonnegative reals, a real number \(\alpha\), a natural number \(a\) and a positive integer \(q\), inequality (1.7) is the condition \(|\alpha - a/q| \le \psi(q)/q\).

def inequality_1_7 (ψ : ℕ+ → ℝ≥0) (α : ℝ) (a : ℕ) (q : ℕ+) : Prop :=
  |α - a / q| ≤ ψ q / q

Used by 2

Used byThe set \(\mathcal{A}\) of the Duffin–Schaeffer conjecture · The set \(\mathcal{K}\) of Catlin's conjecture

DefinitionThe set \(\mathcal{A}\) of the Duffin–Schaeffer conjecture#✓fully proved

For a function \(\psi\) from the positive integers to the nonnegative reals, \(\mathcal{A}(\psi)\) is the set of real numbers \(\alpha \in [0, 1]\) for which inequality (1.7), \(|\alpha - a/q| \le \psi(q)/q\), has infinitely many solutions \((a, q)\) with \(a\) a natural number, \(q\) a positive integer and \(\gcd(a, q) = 1\).

def 𝒜 (ψ : ℕ+ → ℝ≥0) : Set ℝ :=
  {α ∈ Set.Icc 0 1 | {(a, q) : ℕ × ℕ+ | Nat.Coprime a q ∧ inequality_1_7 ψ α a q}.Infinite}

Uses 1 · Used by 2

Statement usesThe approximation inequality (1.7)

Used byKoukoulopoulos–Maynard Corollary 3 (Hausdorff dimension of \(\mathcal{A}\)) · Koukoulopoulos–Maynard Theorem 1 (Duffin–Schaeffer conjecture)

TheoremKoukoulopoulos–Maynard Theorem 1 (Duffin–Schaeffer conjecture)#●ready to prove

Let \(\psi\) be a function from the positive integers to the nonnegative reals such that the series \(\sum_{q \ge 1} \psi(q)\varphi(q)/q\) diverges, where \(\varphi\) is Euler's totient function. Let \(\mathcal{A}(\psi)\) be the set of real numbers \(\alpha \in [0, 1]\) for which \(|\alpha - a/q| \le \psi(q)/q\) has infinitely many solutions with \(a\) a natural number, \(q\) a positive integer and \(\gcd(a, q) = 1\). Then \(\mathcal{A}(\psi)\) is a Borel set and has Lebesgue measure \(1\).

public theorem_wanted theorem_1 (ψ : ℕ+ → ℝ≥0) (hdivergence : ¬ Summable fun q ↦ (ψ q * φ q) / q) :
    MeasurableSet (𝒜 ψ) ∧ volume (𝒜 ψ) = 1

Sources

• D. Koukoulopoulos and J. Maynard, On the Duffin-Schaeffer conjecture, Annals of Math, 192 (1) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_duffin_schaeffer_conjecture of the lean-eval benchmark.

Uses 1

Statement usesThe set \(\mathcal{A}\) of the Duffin–Schaeffer conjecture

DefinitionThe set \(\mathcal{K}\) of Catlin's conjecture#✓fully proved

For a function \(\psi\) from the positive integers to the nonnegative reals, \(\mathcal{K}(\psi)\) is the set of real numbers \(\alpha \in [0, 1]\) for which inequality (1.7), \(|\alpha - a/q| \le \psi(q)/q\), has infinitely many solutions \((a, q)\) with \(a\) a natural number and \(q\) a positive integer such that \(a \le q\).

The fractions \(a/q\) need not be reduced.

def 𝒦 (ψ : ℕ+ → ℝ≥0) : Set ℝ :=
  {α ∈ Set.Icc 0 1 | {(a, q) : ℕ × ℕ+ | a ≤ q ∧ inequality_1_7 ψ α a q}.Infinite}

Uses 1 · Used by 2

Statement usesThe approximation inequality (1.7)

Used byKoukoulopoulos–Maynard Theorem 2(a) (Catlin's conjecture, convergent case) · Koukoulopoulos–Maynard Theorem 2(b) (Catlin's conjecture, divergent case)

DefinitionThe function \(\psi^*\) of Catlin's conjecture#✓fully proved

The function \(\psi^*\) of Catlin's conjecture. For a function \(\psi\) from the positive integers to the nonnegative reals, \(\psi^*\) sends each positive integer \(q\) to \(\psi^*(q) = \varphi(q) \cdot \sup \{\psi(n)/n : n \text{ a positive integer with } q \mid n\}\), where \(\varphi\) is Euler's totient function and the supremum is taken in \([0, \infty]\).

noncomputable def ψ_star (ψ : ℕ+ → ℝ≥0) : ℕ+ → ℝ≥0∞ :=
  fun q ↦ φ q * sSup {r : ℝ≥0∞ | ∃ n : ℕ+, q ∣ n ∧ r = ψ n / n}

Used by 2

Used byKoukoulopoulos–Maynard Theorem 2(a) (Catlin's conjecture, convergent case) · Koukoulopoulos–Maynard Theorem 2(b) (Catlin's conjecture, divergent case)

TheoremKoukoulopoulos–Maynard Theorem 2(a) (Catlin's conjecture, convergent case)#●ready to prove

Let \(\psi\) be a function from the positive integers to the nonnegative reals, and for each positive integer \(q\) let \(\psi^*(q) = \varphi(q) \cdot \sup \{\psi(n)/n : n \text{ a positive integer with } q \mid n\}\), where \(\varphi\) is Euler's totient function and the supremum is taken in \([0, \infty]\). Let \(\mathcal{K}(\psi)\) be the set of real numbers \(\alpha \in [0, 1]\) for which \(|\alpha - a/q| \le \psi(q)/q\) has infinitely many solutions with \(a\) a natural number and \(q\) a positive integer such that \(a \le q\). If \(\sum_{q \ge 1} \psi^*(q) < \infty\), then \(\mathcal{K}(\psi)\) is a Borel set and has Lebesgue measure \(0\).

public theorem_wanted theorem_2_a (ψ : ℕ+ → ℝ≥0) (hψ : ∑' q, ψ_star ψ q < ∞) :
    MeasurableSet (𝒦 ψ) ∧ volume (𝒦 ψ) = 0

Sources

• D. Koukoulopoulos and J. Maynard, On the Duffin-Schaeffer conjecture, Annals of Math, 192 (1) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_duffin_schaeffer_conjecture of the lean-eval benchmark.

Uses 2

Statement usesThe function \(\psi^*\) of Catlin's conjecture · The set \(\mathcal{K}\) of Catlin's conjecture

TheoremKoukoulopoulos–Maynard Theorem 2(b) (Catlin's conjecture, divergent case)#●ready to prove

Let \(\psi\) be a function from the positive integers to the nonnegative reals, and for each positive integer \(q\) let \(\psi^*(q) = \varphi(q) \cdot \sup \{\psi(n)/n : n \text{ a positive integer with } q \mid n\}\), where \(\varphi\) is Euler's totient function and the supremum is taken in \([0, \infty]\). Let \(\mathcal{K}(\psi)\) be the set of real numbers \(\alpha \in [0, 1]\) for which \(|\alpha - a/q| \le \psi(q)/q\) has infinitely many solutions with \(a\) a natural number and \(q\) a positive integer such that \(a \le q\). If \(\sum_{q \ge 1} \psi^*(q) = \infty\), then \(\mathcal{K}(\psi)\) is a Borel set and has Lebesgue measure \(1\).

public theorem_wanted theorem_2_b (ψ : ℕ+ → ℝ≥0) (hψ : ∑' q, ψ_star ψ q = ∞) :
    MeasurableSet (𝒦 ψ) ∧ volume (𝒦 ψ) = 1

Sources

• D. Koukoulopoulos and J. Maynard, On the Duffin-Schaeffer conjecture, Annals of Math, 192 (1) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_duffin_schaeffer_conjecture of the lean-eval benchmark.

Uses 2

Statement usesThe function \(\psi^*\) of Catlin's conjecture · The set \(\mathcal{K}\) of Catlin's conjecture

DefinitionThe convergence exponent \(s(\psi)\)#✓fully proved

For a function \(\psi\) from the positive integers to the nonnegative reals, \(s(\psi)\) is the infimum, taken in the nonnegative reals, of the set of real numbers \(\beta \ge 0\) for which the series \(\sum_{q \ge 1} \varphi(q) (\psi(q)/q)^{\beta}\) converges, where \(\varphi\) is Euler's totient function. If there is no such \(\beta\), then \(s(\psi) = 0\).

noncomputable def s_inf (ψ : ℕ+ → ℝ≥0) : ℝ≥0 :=
  sInf {β | Summable fun q : ℕ+ ↦ φ q * (ψ q / q) ^ β.1}

Used by 1

Used byKoukoulopoulos–Maynard Corollary 3 (Hausdorff dimension of \(\mathcal{A}\))

TheoremKoukoulopoulos–Maynard Corollary 3 (Hausdorff dimension of \(\mathcal{A}\))#●ready to prove

Let \(\psi\) be a function from the positive integers to \([0, 1/2]\). Let \(\mathcal{A}(\psi)\) be the set of real numbers \(\alpha \in [0, 1]\) for which \(|\alpha - a/q| \le \psi(q)/q\) has infinitely many solutions with \(a\) a natural number, \(q\) a positive integer and \(\gcd(a, q) = 1\). Let \(s(\psi)\) be the infimum, taken in the nonnegative reals (where the empty set has infimum \(0\)), of the real numbers \(\beta \ge 0\) for which the series \(\sum_{q \ge 1} \varphi(q) (\psi(q)/q)^{\beta}\) converges, where \(\varphi\) is Euler's totient function. Then the Hausdorff dimension of \(\mathcal{A}(\psi)\) equals \(\min(s(\psi), 1)\).

public theorem_wanted corollary_3 (ψ : ℕ+ → ℝ≥0) (hψ : ∀ n, ψ n ∈ Set.Icc 0 (1 / 2)) :
    dimH (𝒜 ψ) = min (s_inf ψ) 1

Sources

• D. Koukoulopoulos and J. Maynard, On the Duffin-Schaeffer conjecture, Annals of Math, 192 (1) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_duffin_schaeffer_conjecture of the lean-eval benchmark.

Uses 2

Statement usesThe convergence exponent \(s(\psi)\) · The set \(\mathcal{A}\) of the Duffin–Schaeffer conjecture

TheoremDuffin–Schaeffer conjecture on the unit circle#●ready to prove

Let \((\delta_n)_{n \in \mathbb{N}}\) be a sequence of nonnegative real numbers. Let \(W\) be the set of points \(x\) of the circle \(\mathbb{R}/\mathbb{Z}\) such that, for infinitely many positive integers \(n\), the distance from \(x\) to some point of additive order exactly \(n\) is less than \(\delta_n\). Then \(W\) has measure \(1\) for the Haar measure of total mass \(1\) on \(\mathbb{R}/\mathbb{Z}\) if and only if the series \(\sum_{n} \varphi(n)\,\delta_n\) diverges, where \(\varphi\) is Euler's totient function.

The points of additive order exactly \(n\) are the reduced fractions \(a/n\) modulo \(1\).

public theorem_wanted duffin_schaeffer (δ : ℕ → ℝ) (hδ : ∀ n, 0 ≤ δ n) :
    volume (addWellApproximable UnitAddCircle δ) = 1 ↔
      ¬ Summable fun n : ℕ => n.totient * δ n

Sources

• D. Koukoulopoulos and J. Maynard, 'On the Duffin-Schaeffer conjecture', Ann. of Math. 192 (2020), 251-307, https://doi.org/10.4007/annals.2020.192.1.5. Problem duffin_schaeffer of the lean-eval benchmark.

5 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.