volume_iUnion_setOf_liouvilleWith
theorem volume_iUnion_setOf_liouvilleWith : ↑↑MeasureTheory.volume (⋃ p, ⋃ (_ : 2 < p), {x | LiouvilleWith p x}) = 0
The theorem `volume_iUnion_setOf_liouvilleWith` states that the set of numbers which satisfy the Liouville's condition with any exponent `p > 2` has a Lebesgue measure of zero. In other words, the measure (size) of the set of all Liouville numbers `x` for which there exists a real number `p > 2`, such that `x` satisfies the Liouville's condition with exponent `p`, is equal to zero according to the Lebesgue measure theory. The Liouville's condition here refers to the existence of a real number `C` such that for infinitely many natural numbers `n`, there exists an integer `m` where `x ≠ m / n` and the absolute value of `x - m / n` is less than `C / n ^ p`.
More concisely: The set of Liouville numbers, which are real numbers satisfying the Liouville condition with some exponent `p > 2`, has Lebesgue measure zero.
|
volume_setOf_liouville
theorem volume_setOf_liouville : ↑↑MeasureTheory.volume {x | Liouville x} = 0
This theorem states that the set of Liouville numbers has a Lebesgue measure of zero. In other words, although there are infinitely many Liouville numbers, they occupy a negligible "volume" on the real number line when measured using the Lebesgue measure.
More concisely: The set of Liouville numbers has Lebesgue measure zero.
|
Real.disjoint_residual_ae
theorem Real.disjoint_residual_ae : Disjoint (residual ℝ) MeasureTheory.volume.ae
The theorem `Real.disjoint_residual_ae` states that the filters `residual ℝ` and `volume.ae` are disjoint. In other words, there exists a set in the real numbers that is residual (i.e., it contains a countable intersection of dense open sets) and has Lebesgue measure zero under almost every condition (i.e., except possibly for a set of measure zero). An example of such a set is the set of Liouville numbers.
More concisely: The theorem `Real.disjoint_residual_ae` asserts that the residual set and the set of real numbers of Lebesgue measure zero under almost every condition are disjoint.
|