Volume of the set of Liouville numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Since this set is a residual set, we show that the filters residual and volume.ae 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

source

theorem set_of_liouville_with_subset_aux :

{x : ℝ | ∃ (p : ℝ) (H : p > 2), liouville_with p x} ⊆ ⋃ (m : ℤ), (λ (x : ℝ), x + ↑m) ⁻¹' ⋃ (n : ℕ) (H : n > 0), {x : ℝ | ∃ᶠ (b : ℕ) in filter.at_top , ∃ (a : ℤ) (H : a ∈ finset.Icc 0 ↑b), |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}

source

@[simp]

theorem volume_Union_set_of_liouville_with :

⇑measure_theory.measure_space.volume (⋃ (p : ℝ) (hp : 2 < p), {x : ℝ | liouville_with p x}) = 0

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

source

theorem ae_not_liouville_with :

∀ᵐ (x : ℝ), ∀ (p : ℝ), p > 2 → ¬liouville_with p x

source

theorem ae_not_liouville :

∀ᵐ (x : ℝ), ¬liouville x

source

@[simp]

theorem volume_set_of_liouville :

⇑measure_theory.measure_space.volume {x : ℝ | liouville x} = 0

The set of Liouville numbers has Lebesgue measure zero.

source

theorem real.disjoint_residual_ae :

disjoint (residual ℝ) measure_theory.measure_space.volume.ae

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