Volume of the set of Liouville numbers

In this file we prove that the set of Liouville numbers with exponent (irrationality measure) strictly greater than two is a set of Lebesgue measure zero, see volume_iUnion_setOfPred_liouvilleWith.

Since this set is a residual set, we show that the filters residual and ae volume are disjoint. These filters correspond to two common notions of genericity on ℝ: residual sets and sets of full measure. The fact that the filters are disjoint means that two mutually exclusive properties can be “generic” at the same time (in the sense of different “genericity” filters).

Tags

Liouville number, Lebesgue measure, residual, generic property

theorem setOfPred_liouvilleWith_subset_aux : {x : ℝ | ∃ p > 2, LiouvilleWith p x} ⊆ ⋃ (m : ℤ), (fun (x : ℝ) => x + ↑m) ⁻¹' ⋃ (n : ℕ), ⋃ (_ : n > 0), {x : ℝ | ∃ᶠ (b : ℕ) in Filter.atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}

@[deprecated setOfPred_liouvilleWith_subset_aux (since := "2026-07-09")]

theorem setOf_liouvilleWith_subset_aux : {x : ℝ | ∃ p > 2, LiouvilleWith p x} ⊆ ⋃ (m : ℤ), (fun (x : ℝ) => x + ↑m) ⁻¹' ⋃ (n : ℕ), ⋃ (_ : n > 0), {x : ℝ | ∃ᶠ (b : ℕ) in Filter.atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}

Alias of setOfPred_liouvilleWith_subset_aux.

@[simp]

theorem volume_iUnion_setOfPred_liouvilleWith : MeasureTheory.volume (⋃ (p : ℝ), ⋃ (_ : 2 < p), {x : ℝ | LiouvilleWith p x}) = 0

The set of numbers satisfying the Liouville condition with some exponent p > 2 has Lebesgue measure zero.

@[deprecated volume_iUnion_setOfPred_liouvilleWith (since := "2026-07-09")]

theorem volume_iUnion_setOf_liouvilleWith : MeasureTheory.volume (⋃ (p : ℝ), ⋃ (_ : 2 < p), {x : ℝ | LiouvilleWith p x}) = 0

Alias of volume_iUnion_setOfPred_liouvilleWith.

---

The set of numbers satisfying the Liouville condition with some exponent p > 2 has Lebesgue measure zero.

theorem ae_not_liouvilleWith : ∀ᵐ (x : ℝ), ∀ p > 2, ¬LiouvilleWith p x

theorem ae_not_liouville : ∀ᵐ (x : ℝ), ¬Liouville x

@[simp]

theorem volume_setOfPred_liouville : MeasureTheory.volume {x : ℝ | Liouville x} = 0

The set of Liouville numbers has Lebesgue measure zero.

@[deprecated volume_setOfPred_liouville (since := "2026-07-09")]

theorem volume_setOf_liouville : MeasureTheory.volume {x : ℝ | Liouville x} = 0

Alias of volume_setOfPred_liouville.

---

The set of Liouville numbers has Lebesgue measure zero.

theorem Real.disjoint_residual_ae : Disjoint (residual ℝ) (MeasureTheory.ae MeasureTheory.volume)

The filters residual ℝ and ae volume are disjoint. This means that there exists a residual set of Lebesgue measure zero (e.g., the set of Liouville numbers).