On the Duffin-Schaeffer conjecture
Loading leaderboard data…
Problem statement
Notes: In the paper, `ℕ` denotes the positive integers, which are denoted `ℕ+` in Lean. Hence, no changes to the domains of the functions `ψ` and `ψ⋆` have been made in the formalisation. LeanEval changes `lemma corollary_3` to `theorem corollary_3` because the workspace generator addresses theorem holes by that keyword; this does not change the declaration's type.
Source: D. Koukoulopoulos and J. Maynard, `On the Duffin-Schaeffer conjecture`, Annals of Math, 192 (1) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2020-192-1-DuffinSchaefferConjecture.lean
Informal solution: Unavailable.
/--
Statement of Theorem 1:
If for `ψ : ℕ → ℝ≥0`, the infinite series `∑ (ψ q * φ q) / q`, where `φ` is the
Euler totient function, diverges, then the set `𝒜` defined above has Lebesgue measure `1`.
-/
theorem declaration uses `sorry`theorem_1 (ψ : ℕ+ → ℝ≥0) (hdivergence : ¬ Summable fun q ↦ (ψ q * φ q) / q) :
MeasurableSet (𝒜 ψ) ∧ volume (𝒜 ψ) = 1 := ψ:ℕ+ → ℝ≥0hdivergence:¬Summable fun q => ψ q * ↑(φ ↑q) / ↑↑q⊢ MeasurableSet (𝒜 ψ) ∧ volume (𝒜 ψ) = 1
All goals completed! 🐙/--
Statement of Theorem 2(a):
Let `ψ : ℕ → ℝ≥0`, `𝒦` and `ψ⋆` be as above. Then, if `∑ ψ⋆ (q)` converges, `𝒦` has Lebesgue
measure `0`.
-/
theorem declaration uses `sorry`theorem_2_a (ψ : ℕ+ → ℝ≥0) (hψ : ∑' q, ψ_star ψ q < ∞) :
MeasurableSet (𝒦 ψ) ∧ volume (𝒦 ψ) = 0 := ψ:ℕ+ → ℝ≥0hψ:∑' (q : ℕ+), ψ_star ψ q < ∞⊢ MeasurableSet (𝒦 ψ) ∧ volume (𝒦 ψ) = 0
All goals completed! 🐙/--
Statement of Theorem 2(b):
Let `ψ : ℕ → ℝ≥0`, `𝒦` and `ψ⋆` be as above. Then, if `∑ ψ⋆ (q)` diverges, `𝒦` has Lebesgue
measure `1`.
-/
theorem declaration uses `sorry`theorem_2_b (ψ : ℕ+ → ℝ≥0) (hψ : ∑' q, ψ_star ψ q = ∞) :
MeasurableSet (𝒦 ψ) ∧ volume (𝒦 ψ) = 1 := ψ:ℕ+ → ℝ≥0hψ:∑' (q : ℕ+), ψ_star ψ q = ∞⊢ MeasurableSet (𝒦 ψ) ∧ volume (𝒦 ψ) = 1
All goals completed! 🐙/--
Statement of Corollary 3:
For a function `ψ : ℕ → [0, 1/2]`, the set `𝒜` and the element `s` defined as above,
the Hausdorff dimension of `𝒜` is the minimum of `s` and `1`.
-/
theorem declaration uses `sorry`corollary_3 (ψ : ℕ+ → ℝ≥0) (hψ : ∀ n, ψ n ∈ Set.Icc 0 (1 / 2)) :
dimH (𝒜 ψ) = min (s_inf ψ) 1 := ψ:ℕ+ → ℝ≥0hψ:∀ (n : ℕ+), ψ n ∈ Set.Icc 0 (1 / 2)⊢ dimH (𝒜 ψ) = ↑(min (s_inf ψ) 1)
All goals completed! 🐙