Lebesgue measure

Lebesgue measure on the real line and Euclidean space: volumes of concrete bodies, null sets and density phenomena.

• Null sets
• Volumes of polytopes

TheoremSets of finite Lebesgue measure contain no right half-line#✓fully proved

Let \(E \subseteq \mathbb{R}\) have finite Lebesgue outer measure (\(E\) need not be measurable). Then for every real \(X\) there is a real \(x > X\) with \(x \notin E\); that is, \(E\) contains no half-line \((X, \infty)\).

theorem exists_gt_not_mem_of_volume_lt_top
    (E : Set ℝ) (hE : volume E < ∞) (X : ℝ) :
    ∃ x : ℝ, X < x ∧ x ∉ E

Used by 1

Used byWiman's inequality with exponent \(2/3\) at arbitrarily large radii

TheoremSets of positive measure contain three-term arithmetic progressions#●ready to prove

For every Borel set \(A \subseteq \mathbb{R}\) of positive Lebesgue measure there exist \(x \in A\) and \(y > 0\) such that \(x + y \in A\) and \(x - y \in A\).

public theorem_wanted exists_add_mem_and_sub_mem_of_volume_pos
    (A : Set ℝ) (hAmeas : MeasurableSet A) (hApos : (0 : ENNReal) < volume A) :
    ∃ x ∈ A, ∃ y : ℝ, 0 < y ∧ x + y ∈ A ∧ x - y ∈ A

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem ma_proofbench_l2_75.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.