Introduction to Measure Theory, Section 1.2.1: Properties of Lebesgue outer measure

A companion to (the introduction to) Section 1.2.1 of the book "An introduction to Measure Theory".

theorem Lebesgue_outer_measure.of_empty (d : ℕ) : Lebesgue_outer_measure ∅ = 0

Exercise 1.2.3(i) (Empty set)

theorem Lebesgue_outer_measure.mono {d : ℕ} {E F : Set (EuclideanSpace' d)} (h : E ⊆ F) : Lebesgue_outer_measure E ≤ Lebesgue_outer_measure F

Exercise 1.2.3(ii) (Monotonicity)

theorem Lebesgue_outer_measure.nonneg {d : ℕ} (E : Set (EuclideanSpace' d)) : 0 ≤ Lebesgue_outer_measure E

Lebesgue outer measure is non-negative. Since it's the sInf of sums of box volumes, which are all ≥ 0, the result is ≥ 0.

theorem Lebesgue_outer_measure.union_le {d : ℕ} (E : ℕ → Set (EuclideanSpace' d)) : Lebesgue_outer_measure (⋃ (i : ℕ), E i) ≤ ∑' (i : ℕ), Lebesgue_outer_measure (E i)

Exercise 1.2.3(iii) (Countable subadditivity)

theorem Lebesgue_outer_measure.finite_union_le {d n : ℕ} (E : Fin n → Set (EuclideanSpace' d)) : Lebesgue_outer_measure (⋃ (i : Fin n), E i) ≤ ∑ i : Fin n, Lebesgue_outer_measure (E i)

Finite subadditivity

noncomputable def set_dist {X : Type u_1} [PseudoMetricSpace X] (A B : Set X) : ℝ

Equations

• set_dist A B = sInf ((fun (p : X × X) => dist p.1 p.2) '' A ×ˢ B)

def BoundedInterval.endpoints (I : BoundedInterval) : ℝ × ℝ

Extract the left and right endpoints of a BoundedInterval. Returns (a, b) where a is the left endpoint and b is the right endpoint.

Equations

• (BoundedInterval.Ioo a b).endpoints = (a, b)
• (BoundedInterval.Icc a b).endpoints = (a, b)
• (BoundedInterval.Ioc a b).endpoints = (a, b)
• (BoundedInterval.Ico a b).endpoints = (a, b)

noncomputable def BoundedInterval.midpoint (I : BoundedInterval) : ℝ

Compute the midpoint of a BoundedInterval.

Equations

• I.midpoint = match I.endpoints with | (a, b) => (a + b) / 2

noncomputable def BoundedInterval.bisect (I : BoundedInterval) : BoundedInterval × BoundedInterval

Bisect a BoundedInterval into left and right halves using closed intervals. Left half: [a, m], Right half: [m, b], where m is the midpoint. Using closed intervals ensures coverage (union equals original) while maintaining measure-theoretic properties (overlap has measure zero).

Equations

• I.bisect = match I.endpoints with | (a, b) => have m := I.midpoint; (BoundedInterval.Icc a m, BoundedInterval.Icc m b)

theorem BoundedInterval.bisect_fst_length (I : BoundedInterval) : I.bisect.1.length = I.length / 2

The left half of bisection has half the original length

theorem BoundedInterval.bisect_snd_length (I : BoundedInterval) : I.bisect.2.length = I.length / 2

The right half of bisection has half the original length

theorem BoundedInterval.bisect_length_sum (I : BoundedInterval) : I.bisect.1.length + I.bisect.2.length = I.length

Bisecting preserves total length

@[simp]

theorem BoundedInterval.bisect_fst_a (I : BoundedInterval) : I.bisect.1.a = I.a

The left endpoint of bisect.fst is I.a

@[simp]

theorem BoundedInterval.bisect_snd_a (I : BoundedInterval) : I.bisect.2.a = I.midpoint

The left endpoint of bisect.snd is I.midpoint

theorem BoundedInterval.midpoint_eq_a_add_half_length (I : BoundedInterval) (h : I.a ≤ I.b) : I.midpoint = I.a + I.length / 2

The midpoint equals a + length/2 when a ≤ b (non-degenerate interval)

theorem BoundedInterval.midpoint_mem_bisect_fst (I : BoundedInterval) (h : (↑I).Nonempty) : I.midpoint ∈ ↑I.bisect.1

The midpoint is in the first half of bisection (as the right endpoint of Icc)

theorem BoundedInterval.midpoint_mem_bisect_snd (I : BoundedInterval) (h : (↑I).Nonempty) : I.midpoint ∈ ↑I.bisect.2

The midpoint is in the second half of bisection (as the left endpoint of Icc)

theorem BoundedInterval.mem_bisect_snd_iff (I : BoundedInterval) (x : ℝ) (hx : x ∈ ↑I) : x ∈ ↑I.bisect.2 ↔ x ≥ I.midpoint

A point is in I.bisect.snd iff it's in I.toSet and at or above the midpoint

theorem BoundedInterval.mem_bisect_fst_iff (I : BoundedInterval) (x : ℝ) (hx : x ∈ ↑I) : x ∈ ↑I.bisect.1 ↔ x ≤ I.midpoint

A point is in I.bisect.fst iff it's in I.toSet and below the midpoint

theorem BoundedInterval.bisect_fst_eq_endpoints {I₁ I₂ : BoundedInterval} (h : I₁.bisect.1 = I₂.bisect.1) : I₁.a = I₂.a ∧ I₁.b = I₂.b

If two intervals have equal bisect.fst, then their endpoints match

theorem BoundedInterval.bisect_snd_eq_endpoints {I₁ I₂ : BoundedInterval} (h : I₁.bisect.2 = I₂.bisect.2) : I₁.a = I₂.a ∧ I₁.b = I₂.b

If two intervals have equal bisect.snd, then their endpoints match

theorem BoundedInterval.bisect_fst_eq_snd_shift {I₁ I₂ : BoundedInterval} (h : I₁.bisect.1 = I₂.bisect.2) : I₁.a = (I₂.a + I₂.b) / 2

Cross-case: if bisect.fst = bisect.snd, the intervals have overlapping midpoint and endpoint

noncomputable def Box.diameter {d : ℕ} (B : Box d) : ℝ

The diameter of a box is the supremum of Euclidean distances between points in the box

Equations

• B.diameter = sSup {r : ℝ | ∃ x ∈ ↑B, ∃ y ∈ ↑B, r = √(∑ i : Fin d, (x i - y i) ^ 2)}

theorem Box.diameter_nonneg {d : ℕ} (B : Box d) : 0 ≤ B.diameter

Diameter is always nonnegative

theorem Box.diameter_of_empty {d : ℕ} (B : Box d) (h : ↑B = ∅) : B.diameter = 0

Empty box has diameter 0

theorem Box.dist_le_diameter {d : ℕ} (B : Box d) {x y : EuclideanSpace' d} (hx : x ∈ ↑B) (hy : y ∈ ↑B) : √(∑ i : Fin d, (x i - y i) ^ 2) ≤ B.diameter

Any two points in a box have Euclidean distance at most the diameter

theorem Box.BoundedInterval.exists_points_with_diff {I : BoundedInterval} (h_nonempty : (↑I).Nonempty) {t : ℝ} (ht_nonneg : 0 ≤ t) (ht : t < I.length) : ∃ x ∈ ↑I, ∃ y ∈ ↑I, t < |x - y|

For any nonempty interval and target value less than the length, we can find two points in the interval with separation exceeding the target. This is the key density fact: achievable differences are dense in [0, length].

theorem Box.diameter_eq_sqrt_sum_sq {d : ℕ} (B : Box d) (h : (↑B).Nonempty) : B.diameter = √(∑ i : Fin d, (B.side i).length ^ 2)

The diameter of a nonempty box equals the diagonal length √(∑ |side i|ₗ²). This is the key fact: the supremum of pairwise distances equals the diagonal. For closed intervals, the diagonal is achieved at corners. For open intervals, the diagonal is the limit (supremum) of achievable distances.

theorem Box.diameter_ge_dist_of_intersects {d : ℕ} (B : Box d) (E F : Set (EuclideanSpace' d)) (hE : (↑B ∩ E).Nonempty) (hF : (↑B ∩ F).Nonempty) : set_dist E F ≤ B.diameter

If a box intersects two sets, any two points (one from each set) in the box have distance at most the diameter

theorem Box.not_intersects_both_of_diameter_lt {d : ℕ} (B : Box d) (E F : Set (EuclideanSpace' d)) (h : B.diameter < set_dist E F) : ¬((↑B ∩ E).Nonempty ∧ (↑B ∩ F).Nonempty)

If B.diameter < set_dist E F, then B cannot intersect both E and F. This is the core geometric fact needed for finite additivity of separated sets.

noncomputable instance Box.instDecidableEq {d : ℕ} : DecidableEq (Box d)

Decidable equality for boxes, needed for Finset operations

Equations

• Box.instDecidableEq = instDecidableEqOfLawfulBEq

noncomputable def Box.subdivide {d : ℕ} (B : Box d) : Finset (Box d)

Subdivide a box by bisecting each coordinate axis, producing 2^d sub-boxes. Each sub-box is formed by taking one half-interval from each coordinate. We use Finset.univ (all possible d-bit patterns) to enumerate all 2^d combinations.

Equations

• One or more equations did not get rendered due to their size.

theorem Box.volume_subdivide {d : ℕ} (B : Box d) : ∑ B' ∈ B.subdivide, B'.volume = B.volume

The volume of a subdivided box equals the sum of its sub-box volumes

theorem Box.subdivide_diameter_bound {d : ℕ} (B : Box d) (hB : (↑B).Nonempty) (B' : Box d) : B' ∈ B.subdivide → B'.diameter ≤ B.diameter / √2

Each sub-box of a subdivision has diameter at most the original diameter divided by √2. This follows because each side is halved, reducing the diagonal by a factor related to √2. Note: The hypothesis that B is nonempty is necessary because bisection always creates closed intervals, which can turn degenerate open intervals (Ioo a a) into nonempty singletons.

noncomputable def Box.subdivide_iter {d : ℕ} (B : Box d) : ℕ → Finset (Box d)

Subdivide a box k times, producing a Finset of boxes. After k iterations, each original box becomes up to 2^(d*k) sub-boxes.

Equations

• B.subdivide_iter 0 = {B}
• B.subdivide_iter k.succ = (B.subdivide_iter k).biUnion Box.subdivide

theorem Box.subdivide_iter_zero {d : ℕ} (B : Box d) : B.subdivide_iter 0 = {B}

theorem Box.subdivide_iter_succ {d : ℕ} (B : Box d) (k : ℕ) : B.subdivide_iter (k + 1) = (B.subdivide_iter k).biUnion subdivide

theorem Box.subdivide_side_is_Icc {d : ℕ} (B B' : Box d) (hB' : B' ∈ B.subdivide) (i : Fin d) : ∃ (a : ℝ) (b : ℝ), B'.side i = BoundedInterval.Icc a b

All sides in subdivide (single level) are Icc intervals

theorem Box.subdivide_iter_side_is_Icc {d : ℕ} (B : Box d) (k : ℕ) (B' : Box d) (hB' : B' ∈ B.subdivide_iter (k + 1)) (i : Fin d) : ∃ (a : ℝ) (b : ℝ), B'.side i = BoundedInterval.Icc a b

All sides in subdivide_iter for k ≥ 1 are Icc intervals

theorem Box.subdivide_iter_side_length {d : ℕ} (B : Box d) (k : ℕ) (B' : Box d) (hB' : B' ∈ B.subdivide_iter k) (i : Fin d) : (B'.side i).length = (B.side i).length / 2 ^ k

All boxes in subdivide_iter have the same side lengths at each coordinate

theorem Box.subdivide_one_step_nonempty {d : ℕ} (B : Box d) (hB : (↑B).Nonempty) (B' : Box d) : B' ∈ B.subdivide → (↑B').Nonempty

A nonempty box remains nonempty after subdivision

theorem Box.subdivide_iter_nonempty {d : ℕ} (B : Box d) (hB : (↑B).Nonempty) (k : ℕ) (B' : Box d) : B' ∈ B.subdivide_iter k → (↑B').Nonempty

A nonempty box remains nonempty after k iterations of subdivision

theorem Box.subdivide_iter_side_grid {d : ℕ} (B : Box d) (hB : (↑B).Nonempty) (k : ℕ) (B' : Box d) (hB' : B' ∈ B.subdivide_iter k) (i : Fin d) : ∃ j < 2 ^ k, (B'.side i).a = (B.side i).a + ↑j * ((B.side i).length / 2 ^ k)

Grid alignment: sides in subdivide_iter start at grid positions. Requires nonempty box to ensure sides have a ≤ b (backwards intervals break the formula).

theorem Box.volume_subdivide_iter {d : ℕ} (B : Box d) (hB : (↑B).Nonempty) (k : ℕ) : ∑ B' ∈ B.subdivide_iter k, B'.volume = B.volume

Volume is preserved through iterative subdivision

theorem Box.diameter_subdivide_iter {d : ℕ} (B : Box d) (hB : (↑B).Nonempty) (k : ℕ) (B' : Box d) : B' ∈ B.subdivide_iter k → B'.diameter ≤ B.diameter / √2 ^ k

Diameter bound after k iterations of subdivision. Each iteration reduces diameter by factor of √2.

noncomputable def Box.iter_count {d : ℕ} (B : Box d) (r : ℝ) : ℕ

Number of subdivisions needed to get diameter below threshold r. Each subdivision reduces diameter by factor of √2, so after k iterations: diameter ≤ original_diameter / (√2)^k We need (√2)^k > diameter/r, i.e., k > log(diameter/r) / log(√2) = 2·log₂(diameter/r).

Equations

• B.iter_count r = if B.diameter ≤ 0 then 0 else if B.diameter < r then 0 else ⌈2 * Real.log (B.diameter / r) / Real.log 2⌉₊ + 1

theorem Box.diameter_lt_of_iter_count {d : ℕ} (B : Box d) (hB : (↑B).Nonempty) (r : ℝ) (hr : 0 < r) (B' : Box d) : B' ∈ B.subdivide_iter (B.iter_count r) → B'.diameter < r

After iter_count subdivisions, all sub-boxes have diameter < r

theorem Box.subdivide_iter_covers {d : ℕ} (B : Box d) (k : ℕ) (x : EuclideanSpace' d) (hx : x ∈ ↑B) : ∃ B' ∈ B.subdivide_iter k, x ∈ ↑B'

Subdivided boxes cover the original box: any point in B.toSet is contained in some box in subdivide_iter B k.

theorem Box.volume_nonneg {d : ℕ} (B : Box d) : 0 ≤ B.volume

Box volume is non-negative (product of non-negative interval lengths).

theorem Box.isCompact {d : ℕ} (B : Box d) (h_closed : ∀ (i : Fin d), ∃ (a : ℝ) (b : ℝ), B.side i = BoundedInterval.Icc a b) : IsCompact ↑B

Closed boxes (all sides are Icc) in Euclidean space are compact sets.

theorem Lebesgue_outer_measure.le_of_nat_cover {d : ℕ} (hd : 0 < d) (E : Set (EuclideanSpace' d)) (S : ℕ → Box d) (hcover : E ⊆ ⋃ (n : ℕ), ↑(S n)) : Lebesgue_outer_measure E ≤ ∑' (n : ℕ), ↑(S n).volume

Any ℕ-indexed cover gives an upper bound on outer measure. Follows directly from the infimum definition.

theorem Lebesgue_outer_measure.le_of_finset_cover {d : ℕ} (hd : 0 < d) (E : Set (EuclideanSpace' d)) (I : ℕ → Finset (Box d)) (hcover : E ⊆ ⋃ (n : ℕ), ⋃ B ∈ I n, ↑B) : Lebesgue_outer_measure E ≤ ∑' (n : ℕ), ↑(∑ B ∈ I n, B.volume)

Upper bound from finset-indexed cover: if a set is covered by ⋃ n, ⋃ B ∈ I n, B.toSet where each I n is a finite set of boxes, then the outer measure is bounded by the sum of volumes.

Proof strategy:

1. The sigma type (n : ℕ) × ↑(I n) is countable (and hence encodable)
2. Use Encodable instance to define S : ℕ → Box d via decoding
3. Pad with zero-volume box for invalid decodings
4. Apply le_of_nat_cover and bound the enumerated sum

theorem Lebesgue_outer_measure.exists_cover_close {d : ℕ} (hd : 0 < d) (E : Set (EuclideanSpace' d)) (ε : ℝ) (hε : 0 < ε) (h_finite : Lebesgue_outer_measure E ≠ ⊤) : ∃ (S : ℕ → Box d), E ⊆ ⋃ (n : ℕ), ↑(S n) ∧ ∑' (n : ℕ), ↑(S n).volume ≤ Lebesgue_outer_measure E + ↑ε

For any set with finite outer measure, we can find a cover whose volume is within ε of the outer measure. This follows from the definition of outer measure as an infimum.

theorem Lebesgue_outer_measure.union_of_separated {d : ℕ} (hd : 0 < d) {E F : Set (EuclideanSpace' d)} (hsep : set_dist E F > 0) : Lebesgue_outer_measure (E ∪ F) = Lebesgue_outer_measure E + Lebesgue_outer_measure F

Lemma 1.2.5 (Finite additivity for separated sets). If E and F are separated (dist(E,F) > 0), then m*(E ∪ F) = m*(E) + m*(F).

Proof strategy (from textbook):

1. Direction ≤: Use subadditivity
2. Direction ≥: Show m*(E ∪ F) ≥ m*(E) + m*(F)
   • If m*(E ∪ F) = ⊤, trivial
   • If m*(E ∪ F) < ⊤:
     • Get epsilon-close cover of E ∪ F
     • Refine cover so all boxes have diameter < dist(E,F)
     • Partition boxes into E-intersecting and F-intersecting (disjoint by geometric separation)
     • Sum volumes separately: m*(E) + m*(F) ≤ sum of refined cover ≤ m*(E ∪ F) + ε
     • Take ε → 0 to conclude

theorem dist_of_disj_compact_pos {d : ℕ} (E F : Set (EuclideanSpace' d)) (hE : IsCompact E) (hF : IsCompact F) (hdisj : E ∩ F = ∅) : set_dist E F > 0

Exercise 1.2.4

theorem tsum_geometric_inflate {δ : ℝ} (_hδ : 0 < δ) : ∑' (n : ℕ), δ / 2 ^ (n + 2) = δ / 2

Sum of geometric series δ/2^{n+2} equals δ/2

theorem card_ratio_bound {α : Type u_1} {P_nonempty P : Finset α} (hP_nonempty_sub : P_nonempty ⊆ P) {δ : ℝ} (hδ_pos : 0 < δ) (hcard_pos : 0 < P.card) : ↑P_nonempty.card * (δ / (4 * ↑P.card)) ≤ δ / 4

When P_nonempty ⊆ P, the loss from scaling is bounded by δ/4.

theorem partition_volume_bound {d : ℕ} {P P_nonempty : Finset (Box d)} (_hP_nonempty_sub : P_nonempty ⊆ P) {B' : (B : Box d) → B ∈ P_nonempty → Box d} {ε : ℝ} (_hε_pos : 0 < ε) (h_vol_bound : ∀ (B : Box d) (hB : B ∈ P_nonempty), B.volume ≤ (B' B hB).volume + ε) : ∑ B ∈ P_nonempty, B.volume ≤ ∑ x : { B : Box d // B ∈ P_nonempty }, (B' ↑x ⋯).volume + ↑P_nonempty.card * ε

Sum bound from partition filter: if volumes B' satisfy B.vol ≤ B'.vol + ε, then summing over P_nonempty gives total bound with card * ε term.

theorem injective_of_shrunk_nonempty {d : ℕ} {P P_nonempty : Finset (Box d)} (hP_nonempty_sub : P_nonempty ⊆ P) {B' : (B : Box d) → B ∈ P_nonempty → Box d} (hP_disj : (↑P).PairwiseDisjoint Box.toSet) (h_sub : ∀ (B : Box d) (hB : B ∈ P_nonempty), ↑(B' B hB) ⊆ ↑B) (h_nonempty : ∀ (B : Box d) (hB : B ∈ P_nonempty), (↑(B' B hB)).Nonempty) : Function.Injective fun (x : { B : Box d // B ∈ P_nonempty }) => B' ↑x ⋯

Shrunk boxes B' inherit injectivity from parent boxes' disjointness when B' are nonempty.

theorem BoundedInterval.isBounded (I : BoundedInterval) : Bornology.IsBounded ↑I

Every bounded interval (Ioo, Icc, Ioc, Ico) is a bounded set

theorem Box.isBounded {d : ℕ} (B : Box d) : Bornology.IsBounded ↑B

Every box is bounded (product of bounded intervals)

theorem Box.inflate {d : ℕ} (B : Box d) (δ : ℝ) (hδ : 0 < δ) : ∃ (B' : Box d), ↑B ⊆ interior ↑B' ∧ IsOpen (interior ↑B') ∧ B'.volume ≤ B.volume + δ

Enlarge a box to an open box with controlled volume increase

theorem Box.shrink_to_closed {d : ℕ} (B : Box d) (hB : (↑B).Nonempty) (δ : ℝ) (hδ : 0 < δ) : ∃ (B' : Box d), ↑B' ⊆ ↑B ∧ IsClosed ↑B' ∧ B'.volume ≥ B.volume - δ ∧ (↑B').Nonempty

Shrink a box to a closed sub-box with controlled volume decrease. The output is always nonempty when the input is nonempty.

theorem IsElementary.isBounded {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsElementary E) : Bornology.IsBounded E

Elementary sets are bounded (finite union of bounded boxes)

theorem IsElementary.measure_of_empty_eq {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsElementary E) (hempty : E = ∅) : hE.measure = 0

Elementary measure of empty set is zero (handles proof term mismatch)

theorem IsElementary.iUnion_boxes {d : ℕ} {ι : Type u_1} [Fintype ι] (B : ι → Box d) : IsElementary (⋃ (i : ι), ↑(B i))

Finite indexed union of boxes is elementary (uses IsElementary.union' which takes a finset of sets)

theorem IsElementary.measure_le_finset_boxes_volume' {d : ℕ} (t : Finset ℕ) (B : ℕ → Box d) : ⋯.measure ≤ ∑ n ∈ t, (B n).volume

The measure of a finite union of boxes (indexed by finset membership) is at most the sum of volumes. This is finite subadditivity specialized to boxes with a finset index.

theorem IsElementary.measure_le_cover_sum {d : ℕ} (_hd : 0 < d) {E : Set (EuclideanSpace' d)} (hE : IsElementary E) (S : ℕ → Box d) (hS_cover : E ⊆ ⋃ (n : ℕ), ↑(S n)) : ↑hE.measure ≤ ∑' (n : ℕ), ↑(S n).volume

For any box cover of an elementary set, the sum of volumes bounds the measure from below. This is the key step using Heine-Borel compactness: inflate boxes to open cover, extract finite subcover of compact approximation, use finite subadditivity.

theorem IsElementary.measure_le_outer_measure {d : ℕ} (hd : 0 < d) {E : Set (EuclideanSpace' d)} (hE : IsElementary E) : ↑hE.measure ≤ Lebesgue_outer_measure E

Direction 1: Elementary measure is a lower bound for outer measure (Partition gives a finite cover, outer measure is infimum over covers) Uses measure_le_cover_sum for the core Heine-Borel argument.

theorem IsElementary.outer_measure_le_measure {d : ℕ} (_hd : 0 < d) {E : Set (EuclideanSpace' d)} (hE : IsElementary E) : Lebesgue_outer_measure E ≤ ↑hE.measure

Direction 2: Outer measure is bounded by elementary measure (Uses: m*(E) ≤ J*(E) for bounded E, and J*(E) ≤ hE.measure for elementary E)

theorem Lebesgue_outer_measure.elementary_dim_zero (E : Set (EuclideanSpace' 0)) (hE : IsElementary E) : Lebesgue_outer_measure E = ↑hE.measure

Dimension 0 case of Lemma 1.2.6

theorem Lebesgue_outer_measure.elementary {d : ℕ} (E : Set (EuclideanSpace' d)) (hE : IsElementary E) : Lebesgue_outer_measure E = ↑hE.measure

Lemma 1.2.6 (Outer measure of elementary sets). For any elementary set E, Lebesgue outer measure equals elementary measure.

theorem EuclideanSpace'.uncountable (d : ℕ) (hd : 0 < d) : Uncountable (EuclideanSpace' d)

Cantor's theorem

theorem EuclideanSpace'_dist_eq_Real_dist (x y : EuclideanSpace' 1) : dist x y = dist (EuclideanSpace'.equiv_Real x) (EuclideanSpace'.equiv_Real y)

The distance on EuclideanSpace' 1 equals the distance in ℝ via equiv_Real

theorem preimage_Icc_eq_box (a b : ℝ) : ⇑EuclideanSpace'.equiv_Real ⁻¹' Set.Icc a b = ↑↑(BoundedInterval.Icc a b)

Preimage of closed interval [a,b] under equiv_Real equals the corresponding 1D box

theorem tsum_geometric_eps (ε : ℝ) (_hε : 0 < ε) : ∑' (n : ℕ), ε / 2 ^ (n + 1) = ε

Geometric series: ∑ ε/2^{n+1} = ε

theorem tsum_interval_lengths (ε : ℝ) (hε : 0 < ε) : ∑' (n : ℕ), 2 * ε / 2 ^ (n + 1) = 2 * ε

The sum of interval lengths is 2ε

theorem tsum_interval_summable (ε : ℝ) : Summable fun (n : ℕ) => 2 * ε / 2 ^ (n + 1)

Summability of the geometric series

theorem Lebesgue_outer_measure.of_Icc (a b : ℝ) (hab : a ≤ b) : Lebesgue_outer_measure (⇑EuclideanSpace'.equiv_Real ⁻¹' Set.Icc a b) = ↑(b - a)

Lebesgue outer measure of a closed interval [a,b] equals b - a

theorem Lebesgue_outer_measure.of_Ioo_le (a b : ℝ) (h : a < b) : Lebesgue_outer_measure (⇑EuclideanSpace'.equiv_Real ⁻¹' Set.Ioo a b) ≤ ↑(b - a)

Lebesgue measure of an open interval ≤ length (when a < b)

theorem Jordan_outer_measure_mono {E F : Set (EuclideanSpace' 1)} (hEF : E ⊆ F) (_hF : Bornology.IsBounded F) : Jordan_outer_measure E ≤ Jordan_outer_measure F

Monotonicity of Jordan outer measure, for two bounded sets

theorem Remark_1_2_8.rationals_unit_interval_nonempty : (Set.Icc 0 1 ∩ Set.range fun (q : ℚ) => ↑q).Nonempty

Rationals in [0,1] form a nonempty countable set.

theorem Remark_1_2_8.rationals_unit_interval_countable : (Set.Icc 0 1 ∩ Set.range fun (q : ℚ) => ↑q).Countable

noncomputable def Remark_1_2_8.q_enum : ℕ → { x : ℝ // x ∈ Set.Icc 0 1 ∩ Set.range fun (q : ℚ) => ↑q }

An enumeration function of rationals in [0,1]

Equations

• Remark_1_2_8.q_enum = Remark_1_2_8.q_enum._proof_1.choose

theorem Remark_1_2_8.q_enum_surj : Function.Surjective q_enum

noncomputable def Remark_1_2_8.q (n : ℕ) : ℝ

An enumeration of rationals in [0,1] as real numbers

Equations

• Remark_1_2_8.q n = ↑(Remark_1_2_8.q_enum n)

theorem Remark_1_2_8.q_mem (n : ℕ) : q n ∈ Set.Icc 0 1 ∩ Set.range fun (r : ℚ) => ↑r

theorem Remark_1_2_8.q_in_unit_interval (n : ℕ) : q n ∈ Set.Icc 0 1

theorem Remark_1_2_8.q_surj (x : ℝ) : (x ∈ Set.Icc 0 1 ∩ Set.range fun (r : ℚ) => ↑r) → ∃ (n : ℕ), q n = x

noncomputable def Remark_1_2_8.U_real (ε : ℝ) : Set ℝ

The counterexample set U: union of open intervals around rationals in [0,1]. U(ε) = ⋃_{n:ℕ} (q_n - ε/2^{n+1}, q_n + ε/2^{n+1})

Equations

• Remark_1_2_8.U_real ε = ⋃ (n : ℕ), Set.Ioo (Remark_1_2_8.q n - ε / 2 ^ (n + 1)) (Remark_1_2_8.q n + ε / 2 ^ (n + 1))

noncomputable def Remark_1_2_8.U (ε : ℝ) : Set (EuclideanSpace' 1)

The set U lifted to EuclideanSpace' 1

Equations

• Remark_1_2_8.U ε = ⇑EuclideanSpace'.equiv_Real ⁻¹' Remark_1_2_8.U_real ε

theorem Remark_1_2_8.U_real_isOpen (ε : ℝ) : IsOpen (U_real ε)

U_real is open (union of open intervals)

theorem Remark_1_2_8.U_isOpen (ε : ℝ) : IsOpen (U ε)

U is open in EuclideanSpace' 1

noncomputable def Remark_1_2_8.radius (ε : ℝ) (n : ℕ) : ℝ

The radius at step n

Equations

• Remark_1_2_8.radius ε n = ε / 2 ^ (n + 1)

theorem Remark_1_2_8.U_real_subset (ε : ℝ) (hε : 0 < ε) : U_real ε ⊆ Set.Ioo (-ε) (1 + ε)

U_real is contained in (-ε, 1+ε)

theorem Remark_1_2_8.U_isBounded (ε : ℝ) (hε : 0 < ε) : Bornology.IsBounded (U ε)

U is bounded

theorem Remark_1_2_8.component_lebesgue_le (ε : ℝ) (hε : 0 < ε) (n : ℕ) : Lebesgue_outer_measure (⇑EuclideanSpace'.equiv_Real ⁻¹' Set.Ioo (q n - ε / 2 ^ (n + 1)) (q n + ε / 2 ^ (n + 1))) ≤ ↑(2 * ε / 2 ^ (n + 1))

Bound on each component interval's Lebesgue measure

theorem Remark_1_2_8.U_real_closure_contains_unit_interval (ε : ℝ) (hε : 0 < ε) : Set.Icc 0 1 ⊆ closure (U_real ε)

Closure of U_real contains [0,1] (density of rationals)

@[reducible, inline]

abbrev Remark_1_2_8.unit_interval : BoundedInterval

Unit interval [0,1] as a BoundedInterval

Equations

• Remark_1_2_8.unit_interval = BoundedInterval.Icc 0 1

@[reducible, inline]

abbrev Remark_1_2_8.unit_box_1D : Box 1

Unit box in 1D: [0,1] lifted to Box 1

Equations

• Remark_1_2_8.unit_box_1D = ↑Remark_1_2_8.unit_interval

theorem Remark_1_2_8.unit_interval_eq_box : ⇑EuclideanSpace'.equiv_Real ⁻¹' Set.Icc 0 1 = ↑unit_box_1D

Unit interval as the preimage of [0,1] equals unit box

theorem Remark_1_2_8.unit_box_volume : unit_box_1D.volume = 1

Volume of unit box is 1

theorem Remark_1_2_8.Jordan_outer_unit_box : Jordan_outer_measure ↑unit_box_1D = 1

Jordan outer measure of unit box is 1

theorem Remark_1_2_8.U_closure_contains_unit_box (ε : ℝ) (hε : 0 < ε) : ↑unit_box_1D ⊆ closure (U ε)

Closure of U contains the preimage of [0,1]

theorem Remark_1_2_8.U_jordan_outer_ge (ε : ℝ) (hε : 0 < ε) : Jordan_outer_measure (U ε) ≥ 1

Jordan outer measure of U ≥ 1. Proof uses: density of ℚ → closure(U) ⊇ [0,1] → Jordan_outer(U) ≥ Jordan_outer([0,1]) = 1.

theorem Remark_1_2_8.U_lebesgue_le (ε : ℝ) (hε : 0 < ε) : Lebesgue_outer_measure (U ε) ≤ ↑(2 * ε)

Lebesgue outer measure of U ≤ 2ε (countable subadditivity). U = ⋃_n (q_n - ε/2^{n+1}, q_n + ε/2^{n+1}), each interval has length 2ε/2^{n+1}, and ∑ 2ε/2^{n+1} = 2ε.

Proof structure:

1. Express U as countable union: U = ⋃_n E_n
2. By countable subadditivity (union_le): m*(U) ≤ ∑' m*(E_n)
3. Each component bounded: m*(E_n) ≤ 2ε/2^{n+1} (component_lebesgue_le)
4. Geometric sum: ∑' 2ε/2^{n+1} = 2ε (tsum_interval_lengths)
5. EReal tsum comparison: ∑' m*(E_n) ≤ ∑' (2ε/2^{n+1}) = 2ε

def AlmostDisjoint {d : ℕ} (B B' : Box d) : Prop

Equations

• AlmostDisjoint B B' = (interior ↑B ∩ interior ↑B' = ∅)

theorem IsElementary.measure_of_almostDisjUnion {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsElementary E) (hF : IsElementary F) (h : interior E ∩ interior F = ∅) : ⋯.measure = hE.measure + hF.measure

Measure is additive on unions of elementary sets with disjoint interiors: μ(E ∪ F) = μ(E) + μ(F).

theorem Fin.iUnion_succ_eq_union_last {α : Type u_1} {n : ℕ} (f : Fin (n + 1) → Set α) : ⋃ (i : Fin (n + 1)), f i = (⋃ (i : Fin n), f i.castSucc) ∪ f (last n)

Split a Fin (n+1) indexed union into a Fin n indexed union plus the last element. This is a general helper for induction on finite unions.

theorem AlmostDisjoint.pairwise_castSucc {d n : ℕ} {B : Fin (n + 1) → Box d} (hdisj : Pairwise (Function.onFun AlmostDisjoint B)) : Pairwise (Function.onFun AlmostDisjoint fun (i : Fin n) => B i.castSucc)

When boxes are pairwise almost-disjoint, restricting to the first n boxes preserves this.

theorem AlmostDisjoint.castSucc_last {d n : ℕ} {B : Fin (n + 1) → Box d} (hdisj : Pairwise (Function.onFun AlmostDisjoint B)) (i : Fin n) : AlmostDisjoint (B i.castSucc) (B (Fin.last n))

When boxes are pairwise almost-disjoint, any of the first n is almost-disjoint from the last.

theorem BoundedInterval.interior_closure_subset_closure_interior (I : BoundedInterval) : interior (closure ↑I) ⊆ closure (interior ↑I)

For any BoundedInterval, interior (closure I) ⊆ closure (interior I). This holds because all interval types (Ioo, Icc, Ioc, Ico) have closure = Icc and interior = Ioo, so interior(closure(I)) = Ioo ⊆ Icc = closure(interior(I)).

theorem Box.interior_frontier_eq_empty {d : ℕ} (B : Box d) : interior (frontier ↑B) = ∅

For any box, the interior of its frontier is empty. This holds regardless of whether the box uses closed intervals (Icc), open intervals (Ioo), or half-open intervals, because the frontier of a box is a lower-dimensional set (union of faces).

theorem interior_iUnion_Box_frontier_eq_empty {d n : ℕ} (B : Fin n → Box d) : interior (⋃ (i : Fin n), frontier ↑(B i)) = ∅

The interior of a finite union of box frontiers is empty. This is because each box frontier is a closed set with empty interior, and we can apply interior_union_isClosed_of_interior_empty iteratively.

theorem IsElementary.almost_disjoint {d k : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsElementary E) (B : Fin k → Box d) (hEB : E = ⋃ (i : Fin k), ↑(B i)) (hdisj : Pairwise (Function.onFun AlmostDisjoint B)) : hE.measure = ∑ i : Fin k, (B i).volume

theorem AlmostDisjoint.restrict_fin {d : ℕ} {B : ℕ → Box d} (h : Pairwise (Function.onFun AlmostDisjoint B)) (N : ℕ) : Pairwise (Function.onFun AlmostDisjoint fun (i : Fin N) => B ↑i)

Restricting pairwise almost-disjoint from ℕ to Fin N preserves the property.

theorem EReal.tsum_le_of_sum_range_le {f : ℕ → ℝ} {c : EReal} (hf : ∀ (n : ℕ), 0 ≤ f n) (h : ∀ (N : ℕ), ∑ i ∈ Finset.range N, ↑(f i) ≤ c) : ∑' (n : ℕ), ↑(f n) ≤ c

For nonneg Real sequences, if all partial sums are ≤ c (an EReal bound), then tsum ≤ c. This is the converse direction of EReal.finset_sum_le_tsum.

theorem Lebesgue_outer_measure.union_of_almost_disjoint {d : ℕ} {B : ℕ → Box d} (h : Pairwise (Function.onFun AlmostDisjoint B)) : Lebesgue_outer_measure (⋃ (i : ℕ), ↑(B i)) = ∑' (i : ℕ), Lebesgue_outer_measure ↑(B i)

Lemma 1.2.9 (Outer measure of countable unions of almost disjoint boxes). For pairwise almost disjoint boxes, m*(⋃ Bᵢ) = ∑' m*(Bᵢ) = ∑' |Bᵢ|.

theorem Lebesgue_outer_measure.univ {d : ℕ} {hd : 0 < d} : Lebesgue_outer_measure Set.univ = ⊤

theorem Box.sum_volume_eq {d : ℕ} (B B' : ℕ → Box d) (hdisj : Pairwise (Function.onFun AlmostDisjoint B)) (hdisj' : Pairwise (Function.onFun AlmostDisjoint B')) (hcover : ⋃ (n : ℕ), ↑(B n) = ⋃ (n : ℕ), ↑(B' n)) : ∑' (n : ℕ), (B n).volume = ∑' (n : ℕ), (B' n).volume

Remark 1.2.10

theorem Lebesgue_outer_measure.eq_Jordan_inner_of_boxes {d : ℕ} (E : Set (EuclideanSpace' d)) (B : ℕ → Box d) (hE : E = ⋃ (n : ℕ), ↑(B n)) (hdisj : Pairwise (Function.onFun AlmostDisjoint B)) : Lebesgue_outer_measure E = ↑(Jordan_inner_measure E)

Exercise 1.2.5: For any set that equals a countable union of almost disjoint boxes, the Lebesgue outer measure equals the Jordan inner measure.

def IsCube {d : ℕ} (B : Box d) : Prop

Equations

• IsCube B = ∃ (r : ℝ), ∀ (i : Fin d), (B.side i).length = r

noncomputable def DyadicCube {d : ℕ} (n : ℤ) (a : Fin d → ℤ) : Box d

Equations

• DyadicCube n a = { side := fun (i : Fin d) => BoundedInterval.Icc (↑(a i) / 2 ^ n) ((↑(a i) + 1) / 2 ^ n) }

theorem DyadicCube.isCube {d : ℕ} (n : ℤ) (a : Fin d → ℤ) : IsCube (DyadicCube n a)

def Box.IsDyadicAtScale {d : ℕ} (B : Box d) (n : ℤ) : Prop

Equations

• B.IsDyadicAtScale n = ∃ (a : Fin d → ℤ), B = DyadicCube n a

def Box.IsDyadic {d : ℕ} (B : Box d) : Prop

Equations

• B.IsDyadic = ∃ (n : ℕ), B.IsDyadicAtScale ↑n

theorem Box.IsDyadic.all_sides_Icc {d : ℕ} {B : Box d} (hB : B.IsDyadic) (i : Fin d) : ∃ (a : ℝ) (b : ℝ), B.side i = BoundedInterval.Icc a b

Dyadic boxes have all sides as closed intervals (Icc).

theorem DyadicCube.sidelength {d : ℕ} (n : ℤ) (a : Fin d → ℤ) (i : Fin d) : ((DyadicCube n a).side i).length = 2 ^ (-n)

The sidelength of a dyadic cube at scale n is 2^(-n).

theorem DyadicCube.sidelength_le_one {d n : ℕ} (a : Fin d → ℤ) (i : Fin d) : ((DyadicCube (↑n) a).side i).length ≤ 1

Dyadic cubes at scale n ≥ 0 have sidelength at most 1.

theorem DyadicCube.interior {d : ℕ} (n : ℤ) (a : Fin d → ℤ) : _root_.interior ↑(DyadicCube n a) = Set.univ.pi fun (i : Fin d) => Set.Ioo (↑(a i) / 2 ^ n) ((↑(a i) + 1) / 2 ^ n)

The interior of a dyadic cube.

theorem DyadicCube.almost_disjoint_same_scale {d : ℕ} {n : ℤ} {a b : Fin d → ℤ} (hab : a ≠ b) : AlmostDisjoint (DyadicCube n a) (DyadicCube n b)

Dyadic cubes at the same scale with different indices have disjoint interiors.

theorem DyadicCube.cover_univ {d : ℕ} (n : ℤ) : ⋃ (a : Fin d → ℤ), ↑(DyadicCube n a) = Set.univ

The dyadic cubes at scale n cover all of ℝᵈ.

theorem DyadicCube.pairwise_almost_disjoint {d : ℕ} (n : ℤ) : Pairwise (Function.onFun AlmostDisjoint (DyadicCube n))

Dyadic cubes at the same scale are pairwise almost disjoint.

theorem DyadicCube.nesting {d : ℕ} {n m : ℤ} {a b : Fin d → ℤ} : AlmostDisjoint (DyadicCube n a) (DyadicCube m b) ∨ ↑(DyadicCube n a) ⊆ ↑(DyadicCube m b) ∨ ↑(DyadicCube m b) ⊆ ↑(DyadicCube n a)

Two dyadic cubes are either almost disjoint or one contains the other.

theorem IsOpen.exists_dyadic_cube_subset {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsOpen E) {x : EuclideanSpace' d} (hx : x ∈ E) : ∃ (n : ℕ) (a : Fin d → ℤ), x ∈ ↑(DyadicCube (↑n) a) ∧ ↑(DyadicCube (↑n) a) ⊆ E

For any point x in an open set E, there exists a dyadic cube containing x with the cube contained in E.

noncomputable def dyadicCubeContaining {d : ℕ} (n : ℤ) (x : EuclideanSpace' d) : Box d

For a point x, the unique dyadic cube at scale n containing x.

Equations

• dyadicCubeContaining n x = DyadicCube n fun (i : Fin d) => ⌊x i * 2 ^ n⌋

theorem dyadicCubeContaining_mem {d : ℕ} (n : ℤ) (x : EuclideanSpace' d) : x ∈ ↑(dyadicCubeContaining n x)

The dyadic cube containing x at scale n indeed contains x.

theorem dyadicCubeInteriorNonempty {d : ℕ} (n : ℤ) (a : Fin d → ℤ) : (interior ↑(DyadicCube n a)).Nonempty

The interior of a dyadic cube is nonempty.

theorem dyadicCubeNoProperContainmentSameScale {d : ℕ} {n : ℤ} {a b : Fin d → ℤ} (h_sub : ↑(DyadicCube n a) ⊆ ↑(DyadicCube n b)) : a = b

At the same scale, dyadic cubes with different indices cannot have one contained in the other (since containment would imply empty interior for one).

theorem dyadicCubeLargerNotInSmaller {d : ℕ} (hd : 0 < d) {n m : ℤ} (hnm : n < m) {a b : Fin d → ℤ} : ¬↑(DyadicCube n a) ⊆ ↑(DyadicCube m b)

A larger dyadic cube (coarser scale n) cannot be contained in a smaller dyadic cube (finer scale m) when d > 0. This is because the sidelength 2^(-n) > 2^(-m) when n < m.

theorem IsOpen.eq_union_boxes {d : ℕ} (hd : 0 < d) (E : Set (EuclideanSpace' d)) (hE : IsOpen E) (hE_nonempty : E.Nonempty) : ∃ (B : ℕ → Box d), E = ⋃ (n : ℕ), ↑(B n) ∧ (∀ (n : ℕ), (B n).IsDyadic) ∧ Pairwise (Function.onFun AlmostDisjoint B)

Lemma 1.2.11: Every open set is a countable union of almost disjoint dyadic cubes. Note: every dyadic cube is nonempty Proof outline: 1. For each x ∈ E, by exists_dyadic_cube_subset, there exists a dyadic cube containing x ⊆ E 2. The set of all such dyadic cubes is countable (subset of ℕ × (Fin d → ℤ)) 3. Take maximal cubes (not strictly contained in another cube in the collection) 4. By DyadicCube.nesting, distinct maximal cubes are almost disjoint 5. E equals the union of these maximal cubes

theorem Lebesgue_outer_measure.of_open {d : ℕ} (E : Set (EuclideanSpace' d)) (hE : IsOpen E) : Lebesgue_outer_measure E = ↑(Jordan_inner_measure E)

theorem Lebesgue_outer_measure.eq {d : ℕ} (E : Set (EuclideanSpace' d)) : Lebesgue_outer_measure E = sInf {M : EReal | ∃ (U : Set (EuclideanSpace' d)), E ⊆ U ∧ IsOpen U ∧ M = Lebesgue_outer_measure U}

Lemma 1.2.12 (Outer regularity). Proof has not been formalized yet.

theorem Lebesgue_outer_measure.exists_open_superset_measure_le {d : ℕ} (E : Set (EuclideanSpace' d)) (ε : EReal) (hε : 0 < ε) : ∃ (U : Set (EuclideanSpace' d)), IsOpen U ∧ E ⊆ U ∧ Lebesgue_outer_measure U ≤ Lebesgue_outer_measure E + ε

For any set E and ε > 0, there exists an open U ⊇ E with m*(U) ≤ m*(E) + ε. This follows from outer regularity (Lemma 1.2.12).

theorem Lebesgue_outer_measure.finite_of_compact {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsCompact E) : Lebesgue_outer_measure E ≠ ⊤

Compact sets in Euclidean space have finite Lebesgue outer measure.