Introduction to Measure Theory, Section 1.1.1: Elementary measure

A companion to Section 1.1.1 of the book "An introduction to Measure Theory".

inductive BoundedInterval : Type

• Ioo (a b : ℝ) : BoundedInterval
• Icc (a b : ℝ) : BoundedInterval
• Ioc (a b : ℝ) : BoundedInterval
• Ico (a b : ℝ) : BoundedInterval

def BoundedInterval.toSet (I : BoundedInterval) : Set ℝ

Coerces a BoundedInterval to its underlying set of real numbers.

Equations

• ↑(BoundedInterval.Ioo a b) = Set.Ioo a b
• ↑(BoundedInterval.Icc a b) = Set.Icc a b
• ↑(BoundedInterval.Ioc a b) = Set.Ioc a b
• ↑(BoundedInterval.Ico a b) = Set.Ico a b

instance BoundedInterval.inst_coeSet : Coe BoundedInterval (Set ℝ)

Enables coercion from BoundedInterval to Set ℝ.

Equations

• BoundedInterval.inst_coeSet = { coe := BoundedInterval.toSet }

instance BoundedInterval.instEmpty : EmptyCollection BoundedInterval

The empty BoundedInterval is represented as the degenerate open interval (0,0).

Equations

• BoundedInterval.instEmpty = { emptyCollection := BoundedInterval.Ioo 0 0 }

@[simp]

theorem BoundedInterval.coe_empty : ↑∅ = ∅

The empty BoundedInterval coerces to the empty set.

noncomputable instance BoundedInterval.decidableEq : DecidableEq BoundedInterval

This is to make Finsets of BoundedIntervals work properly

Equations

• BoundedInterval.decidableEq = instDecidableEqOfLawfulBEq

@[simp]

theorem BoundedInterval.set_Ioo (a b : ℝ) : ↑(Ioo a b) = Set.Ioo a b

Simp lemmas for coercing each BoundedInterval constructor to Set ℝ.

@[simp]

theorem BoundedInterval.set_Icc (a b : ℝ) : ↑(Icc a b) = Set.Icc a b

@[simp]

theorem BoundedInterval.set_Ioc (a b : ℝ) : ↑(Ioc a b) = Set.Ioc a b

@[simp]

theorem BoundedInterval.set_Ico (a b : ℝ) : ↑(Ico a b) = Set.Ico a b

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

Some helpful general lemmas about BoundedInterval

theorem BoundedInterval.Icc_eq_endpoints {a₁ b₁ a₂ b₂ : ℝ} (h : Set.Icc a₁ b₁ = Set.Icc a₂ b₂) (ha₁b₁ : a₁ ≤ b₁) (ha₂b₂ : a₂ ≤ b₂) : a₁ = a₂ ∧ b₁ = b₂

Extract endpoints from Icc equality

theorem BoundedInterval.Ioo_ne_Icc {a₁ b₁ a₂ b₂ : ℝ} (ha₁b₁ : a₁ < b₁) (ha₂b₂ : a₂ ≤ b₂) : Set.Ioo a₁ b₁ ≠ Set.Icc a₂ b₂

Ioo cannot equal Icc

theorem BoundedInterval.Ioo_ne_Ioc {a₁ b₁ a₂ b₂ : ℝ} (ha₁b₁ : a₁ < b₁) (ha₂b₂ : a₂ < b₂) : Set.Ioo a₁ b₁ ≠ Set.Ioc a₂ b₂

Ioo cannot equal Ioc

theorem BoundedInterval.Ioo_ne_Ico {a₁ b₁ a₂ b₂ : ℝ} (ha₁b₁ : a₁ < b₁) (ha₂b₂ : a₂ < b₂) : Set.Ioo a₁ b₁ ≠ Set.Ico a₂ b₂

Ioo cannot equal Ico

theorem BoundedInterval.Ioc_ne_Ico {a₁ b₁ a₂ b₂ : ℝ} (ha₁b₁ : a₁ < b₁) (ha₂b₂ : a₂ < b₂) : Set.Ioc a₁ b₁ ≠ Set.Ico a₂ b₂

Ioc cannot equal Ico

theorem BoundedInterval.Icc_ne_Ioc {a₁ b₁ a₂ b₂ : ℝ} (ha₁b₁ : a₁ ≤ b₁) (ha₂b₂ : a₂ < b₂) : Set.Icc a₁ b₁ ≠ Set.Ioc a₂ b₂

Icc cannot equal Ioc

theorem BoundedInterval.Icc_ne_Ico {a₁ b₁ a₂ b₂ : ℝ} (ha₁b₁ : a₁ ≤ b₁) (ha₂b₂ : a₂ < b₂) : Set.Icc a₁ b₁ ≠ Set.Ico a₂ b₂

Icc cannot equal Ico

theorem BoundedInterval.toSet_injective_of_nonempty {I J : BoundedInterval} (hI : (↑I).Nonempty) (hJ : (↑J).Nonempty) (h_eq : ↑I = ↑J) : I = J

BoundedInterval.toSet is injective for non-empty intervals

def witness_lowerBound_upperBounds {X : Set ℝ} (y : ℝ) (hy : y ∈ X) : y ∈ lowerBounds (upperBounds X)

A witness for lowerBound of upperBounds

Equations

• ⋯ = ⋯

def witness_upperBound_lowerBounds {X : Set ℝ} (y : ℝ) (hy : y ∈ X) : y ∈ upperBounds (lowerBounds X)

A witness for upperBound of lowerBounds

Equations

• ⋯ = ⋯

theorem exists_gt_of_lt_csSup {X : Set ℝ} (hBddAbove : BddAbove X) (hNonempty : X.Nonempty) (hLowerBound : ∃ y ∈ X, y ∈ lowerBounds (upperBounds X)) (x : ℝ) (hx : x < sSup X) : ∃ z ∈ X, x < z

If x < sSup X, then there exists z ∈ X with x < z

theorem exists_le_of_lt_csInf {X : Set ℝ} (hBddBelow : BddBelow X) (hNonempty : X.Nonempty) (hUpperBound : ∃ y ∈ X, y ∈ upperBounds (lowerBounds X)) (x : ℝ) (hx : sInf X < x) : ∃ w ∈ X, w ≤ x

If sInf X < x, then there exists w ∈ X with w ≤ x

theorem lt_sSup_of_ne_sSup {X : Set ℝ} {x b : ℝ} (_hBddAbove : BddAbove X) (_hb : b = sSup X) (hb_notin : b ∉ X) (hx : x ∈ X) (hx_le_b : x ≤ b) : x < b

Show x < b when b = sSup X and b ∉ X

theorem sInf_lt_of_ne_sInf {X : Set ℝ} {a x : ℝ} (_hBddBelow : BddBelow X) (_ha : a = sInf X) (ha_notin : a ∉ X) (hx : x ∈ X) (ha_le_x : a ≤ x) : a < x

Show a < x when a = sInf X and a ∉ X

theorem mem_of_mem_Icc_ordConnected {X : Set ℝ} (hOrdConn : ∀ ⦃x : ℝ⦄, x ∈ X → ∀ ⦃y : ℝ⦄, y ∈ X → Set.Icc x y ⊆ X) {x w z : ℝ} (hw : w ∈ X) (hz : z ∈ X) (hx : x ∈ Set.Icc w z) : x ∈ X

Use order-connectedness to show x ∈ X when x ∈ [w, z] and w, z ∈ X

theorem BoundedInterval.ordConnected_iff (X : Set ℝ) : Bornology.IsBounded X ∧ X.OrdConnected ↔ ∃ (I : BoundedInterval), X = ↑I

A set of reals is bounded and order-connected if and only if it equals some bounded interval.

theorem BoundedInterval.inter (I J : BoundedInterval) : ∃ (K : BoundedInterval), ↑I ∩ ↑J = ↑K

The intersection of two bounded intervals is again a bounded interval.

noncomputable instance BoundedInterval.instInter : Inter BoundedInterval

Instance enabling ∩ notation for BoundedIntervals.

Equations

• BoundedInterval.instInter = { inter := fun (I J : BoundedInterval) => ⋯.choose }

@[simp]

theorem BoundedInterval.inter_eq (I J : BoundedInterval) : ↑(I ∩ J) = ↑I ∩ ↑J

The intersection of BoundedIntervals equals the set-theoretic intersection.

instance BoundedInterval.instMembership : Membership ℝ BoundedInterval

Instance enabling ∈ notation for membership in BoundedInterval.

Equations

• BoundedInterval.instMembership = { mem := fun (I : BoundedInterval) (x : ℝ) => x ∈ ↑I }

@[simp]

theorem BoundedInterval.mem_iff (I : BoundedInterval) (x : ℝ) : x ∈ I ↔ x ∈ ↑I

Membership in BoundedInterval is equivalent to membership in its underlying set.

instance BoundedInterval.instSubset : HasSubset BoundedInterval

Instance enabling ⊆ notation for BoundedIntervals.

Equations

• BoundedInterval.instSubset = { Subset := fun (I J : BoundedInterval) => ∀ x ∈ I, x ∈ J }

@[simp]

theorem BoundedInterval.subset_iff (I J : BoundedInterval) : I ⊆ J ↔ ↑I ⊆ ↑J

Subset of BoundedIntervals is equivalent to subset of their underlying sets.

@[reducible, inline]

abbrev BoundedInterval.a (I : BoundedInterval) : ℝ

Extracts the left endpoint of a bounded interval.

Equations

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

@[reducible, inline]

abbrev BoundedInterval.b (I : BoundedInterval) : ℝ

Extracts the right endpoint of a bounded interval.

Equations

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

theorem BoundedInterval.nonempty_implies_le (I : BoundedInterval) (h : (↑I).Nonempty) : I.a ≤ I.b

Any nonempty BoundedInterval has a ≤ b

theorem BoundedInterval.subset_Icc (I : BoundedInterval) : I ⊆ Icc I.a I.b

Any bounded interval is contained in the closed interval with the same endpoints.

theorem BoundedInterval.Ioo_subset (I : BoundedInterval) : Ioo I.a I.b ⊆ I

The open interval with the same endpoints is contained in any bounded interval.

@[reducible, inline]

abbrev BoundedInterval.length (I : BoundedInterval) : ℝ

Definition 1.1.1 (boxes): The length of an interval is max(b - a, 0).

Equations

• I.length = max (I.b - I.a) 0

theorem BoundedInterval.length_nonneg (I : BoundedInterval) : 0 ≤ I.length

Length is always non-negative

def «term|___|ₗ» : Lean.ParserDescr

Using ||ₗ subscript here to not override ||

Equations

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

structure Box (d : ℕ) : Type

A d-dimensional box is a Cartesian product of d bounded intervals.

• side : Fin d → BoundedInterval

theorem Box.ext_iff {d : ℕ} {x y : Box d} : x = y ↔ x.side = y.side

theorem Box.ext {d : ℕ} {x y : Box d} (side : x.side = y.side) : x = y

@[reducible, inline]

abbrev Box.toSet {d : ℕ} (B : Box d) : Set (EuclideanSpace' d)

Coerces a Box to its underlying set in d-dimensional Euclidean space.

Equations

• ↑B = Set.univ.pi fun (i : Fin d) => ↑(B.side i)

instance Box.inst_coeSet {d : ℕ} : Coe (Box d) (Set (EuclideanSpace' d))

Enables coercion from Box d to Set (EuclideanSpace' d).

Equations

• Box.inst_coeSet = { coe := Box.toSet }

@[reducible, inline]

abbrev BoundedInterval.toBox (I : BoundedInterval) : Box 1

Lifts a 1-dimensional interval to a 1-dimensional box.

Equations

• ↑I = { side := fun (x : Fin 1) => I }

instance BoundedInterval.inst_coeBox : Coe BoundedInterval (Box 1)

Enables coercion from BoundedInterval to Box 1.

Equations

• BoundedInterval.inst_coeBox = { coe := BoundedInterval.toBox }

@[simp]

theorem BoundedInterval.toBox_inj {I J : BoundedInterval} : ↑I = ↑J ↔ I = J

Coercing to Box 1 is injective: equal boxes implies equal intervals.

@[simp]

theorem BoundedInterval.coe_of_box (I : BoundedInterval) : ↑↑I = ⇑Real.equiv_EuclideanSpace' '' ↑I

A 1D box's set equals the image of the interval under the Real ≃ EuclideanSpace' 1 equivalence.

@[reducible, inline]

abbrev Box.volume {d : ℕ} (B : Box d) : ℝ

Definition 1.1.1 (boxes): The volume of a box is the product of its side lengths.

Equations

• B.volume = ∏ i : Fin d, (B.side i).length

def «term|___|ᵥ» : Lean.ParserDescr

Using ||ᵥ subscript here to not override ||

Equations

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

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

Helper lemma: If a box is empty, its volume is zero

theorem Box.volume_singleton {d : ℕ} (hd : 0 < d) (x : EuclideanSpace' d) : { side := fun (i : Fin d) => BoundedInterval.Icc (x i) (x i) }.volume = 0

A box with all degenerate sides [x, x] has volume 0 when d > 0

theorem Box.side_nonempty_of_nonempty {d : ℕ} (B : Box d) (hB : (↑B).Nonempty) (i : Fin d) : (↑(B.side i)).Nonempty

A nonempty box has nonempty sides at each dimension

@[simp]

theorem Box.volume_of_interval (I : BoundedInterval) : (↑I).volume = I.length

The volume of a 1D box equals the length of the underlying interval.

theorem Box.toSet_injective_of_nonempty {d : ℕ} {B₁ B₂ : Box d} (h₁ : (↑B₁).Nonempty) (h₂ : (↑B₂).Nonempty) (h_eq : ↑B₁ = ↑B₂) : B₁ = B₂

Box.toSet is injective on non-empty boxes

@[reducible, inline]

abbrev IsElementary {d : ℕ} (E : Set (EuclideanSpace' d)) : Prop

A set is elementary if it can be expressed as a finite union of boxes.

Equations

• IsElementary E = ∃ (S : Finset (Box d)), E = ⋃ B ∈ S, ↑B

theorem IsElementary.box {d : ℕ} (B : Box d) : IsElementary ↑B

Every box is an elementary set (witnessed by the singleton finset).

theorem IsElementary.union {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsElementary E) (hF : IsElementary F) : IsElementary (E ∪ F)

Exercise 1.1.1 (Boolean closure): The union of two elementary sets is elementary.

theorem IsElementary.union' {d : ℕ} {S : Finset (Set (EuclideanSpace' d))} (hE : ∀ E ∈ S, IsElementary E) : IsElementary (⋃ E ∈ S, E)

The union of a finset of elementary sets is elementary.

theorem IsElementary.inter {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsElementary E) (hF : IsElementary F) : IsElementary (E ∩ F)

Exercise 1.1.1 (Boolean closure): The intersection of two elementary sets is elementary.

theorem IsElementary.empty (d : ℕ) : IsElementary ∅

The empty set is elementary.

theorem IsElementary.sdiff {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsElementary E) (hF : IsElementary F) : IsElementary (E \ F)

Exercise 1.1.1 (Boolean closure): The set difference of two elementary sets is elementary.

theorem IsElementary.symmDiff {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsElementary E) (hF : IsElementary F) : IsElementary (_root_.symmDiff E F)

Exercise 1.1.1 (Boolean closure): The symmetric difference of two elementary sets is elementary.

theorem IsElementary.translate {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsElementary E) (x : EuclideanSpace' d) : IsElementary (E + {x})

Exercise 1.1.1 (Boolean closure): Translation of an elementary set is elementary.

theorem BoundedInterval.partition (S : Finset BoundedInterval) : ∃ (T : Finset BoundedInterval), (↑T).PairwiseDisjoint toSet ∧ ∀ I ∈ S, ∃ (U : Set { x : BoundedInterval // x ∈ T }), ↑I = ⋃ J ∈ U, ↑↑J

A sublemma for proving Lemma 1.1.2(i): Any finset of intervals admits a common refinement into pairwise disjoint sub-intervals.

theorem Box.partition {d : ℕ} (S : Finset (Box d)) : ∃ (T : Finset (Box d)), (↑T).PairwiseDisjoint toSet ∧ ∀ I ∈ S, ∃ (U : Set { x : Box d // x ∈ T }), ↑I = ⋃ J ∈ U, ↑↑J

Lemma 1.1.2(i): Any finset of boxes admits a common refinement into pairwise disjoint sub-boxes.

theorem IsElementary.partition {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsElementary E) : ∃ (T : Finset (Box d)), (↑T).PairwiseDisjoint Box.toSet ∧ E = ⋃ J ∈ T, ↑J

Every elementary set can be partitioned into pairwise disjoint boxes.

theorem BoundedInterval.sample_finite (I : BoundedInterval) {N : ℕ} (hN : N ≠ 0) : Finite ↑(↑I ∩ Set.range fun (n : ℤ) => (↑N)⁻¹ * ↑n)

Helper lemma for Lemma 1.1.2(ii): The set of lattice points (multiples of 1/N) in an interval is finite.

theorem BoundedInterval.length_eq (I : BoundedInterval) : Filter.Tendsto (fun (N : ℕ) => (↑N)⁻¹ * ↑(Nat.card ↑(↑I ∩ Set.range fun (n : ℤ) => (↑N)⁻¹ * ↑n))) Filter.atTop (nhds I.length)

Exercise for Lemma 1.1.2(ii): Interval length equals the limit of lattice point counts scaled by 1/N.

def Box.sample_congr {d : ℕ} (B : Box d) (N : ℕ) : ↑(↑B ∩ Set.range fun (n : Fin d → ℤ) (i : Fin d) => (↑N)⁻¹ * ↑(n i)) ≃ ((i : Fin d) → ↑(↑(B.side i) ∩ Set.range fun (n : ℤ) => (↑N)⁻¹ * ↑n))

Lattice points in a box decompose as a product of lattice points in each interval side.

Equations

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

theorem Box.sample_finite {d : ℕ} (B : Box d) {N : ℕ} (hN : N ≠ 0) : Finite ↑(↑B ∩ Set.range fun (n : Fin d → ℤ) (i : Fin d) => (↑N)⁻¹ * ↑(n i))

Helper lemma for Lemma 1.1.2(ii): The set of lattice points in a box is finite.

theorem Box.vol_eq {d : ℕ} (B : Box d) : Filter.Tendsto (fun (N : ℕ) => ↑N ^ (-↑d) * ↑(Nat.card ↑(↑B ∩ Set.range fun (n : Fin d → ℤ) (i : Fin d) => (↑N)⁻¹ * ↑(n i)))) Filter.atTop (nhds B.volume)

Helper lemma for Lemma 1.1.2(ii): Box volume equals the limit of lattice point counts scaled by N^(-d).

theorem Box.sum_vol_eq {d : ℕ} {T : Finset (Box d)} (hT : (↑T).PairwiseDisjoint toSet) : Filter.Tendsto (fun (N : ℕ) => ↑N ^ (-↑d) * ↑(Nat.card ↑((⋃ B ∈ T, ↑B) ∩ Set.range fun (n : Fin d → ℤ) (i : Fin d) => (↑N)⁻¹ * ↑(n i)))) Filter.atTop (nhds (∑ B ∈ T, B.volume))

Lemma 1.1.2(ii), helper lemma: Sum of volumes equals limit of lattice counts over a disjoint union.

theorem Box.measure_uniq {d : ℕ} {T₁ T₂ : Finset (Box d)} (hT₁ : (↑T₁).PairwiseDisjoint toSet) (hT₂ : (↑T₂).PairwiseDisjoint toSet) (heq : ⋃ B ∈ T₁, ↑B = ⋃ B ∈ T₂, ↑B) : ∑ B ∈ T₁, B.volume = ∑ B ∈ T₂, B.volume

Lemma 1.1.2(ii): Two disjoint partitions of the same set have equal sums of volumes.

@[reducible, inline]

noncomputable abbrev IsElementary.measure {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsElementary E) : ℝ

The elementary measure of a set, defined as the sum of volumes over a disjoint partition.

Equations

• hE.measure = ∑ B ∈ ⋯.choose, B.volume

theorem IsElementary.measure_eq {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsElementary E) {T : Finset (Box d)} (hT : (↑T).PairwiseDisjoint Box.toSet) (heq : E = ⋃ B ∈ T, ↑B) : hE.measure = ∑ B ∈ T, B.volume

The measure equals the sum of volumes for any disjoint box partition of the set.

theorem Box.measure_uniq' {d : ℕ} {T₁ T₂ : Finset (Box d)} (hT₁ : (↑T₁).PairwiseDisjoint toSet) (hT₂ : (↑T₂).PairwiseDisjoint toSet) (heq : ⋃ B ∈ T₁, ↑B = ⋃ B ∈ T₂, ↑B) : ∑ B ∈ T₁, B.volume = ∑ B ∈ T₂, B.volume

Exercise 1.1.2: give an alternate proof of this proposition by showing that the two partitions T₁, T₂ admit a mutual refinement into boxes arising from taking Cartesian products of elements from finite collections of disjoint intervals.

theorem IsElementary.measure_nonneg {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsElementary E) : 0 ≤ hE.measure

Elementary measure is always non-negative.

theorem IsElementary.measure_of_disjUnion {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsElementary E) (hF : IsElementary F) (hdisj : Disjoint E F) : ⋯.measure = hE.measure + hF.measure

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

theorem IsElementary.measure_irrelevant {d : ℕ} {E : Set (EuclideanSpace' d)} (h₁ h₂ : IsElementary E) : h₁.measure = h₂.measure

Two different proofs that a set is elementary yield the same measure.

theorem IsElementary.measure_eq_of_set_eq {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsElementary E) (hF : IsElementary F) (h : E = F) : hE.measure = hF.measure

If two elementary sets are equal, their measures are equal.

theorem IsElementary.union'_empty_eq {d : ℕ} : ⋃ E ∈ ∅, E = ∅

The union over an empty finset of elementary sets is the empty set.

theorem IsElementary.sum_insert_split {d : ℕ} {a : Set (EuclideanSpace' d)} {S' : Finset (Set (EuclideanSpace' d))} (ha : a ∉ S') (hE : ∀ E ∈ insert a S', IsElementary E) : ∑ E : { x : Set (EuclideanSpace' d) // x ∈ insert a S' }, ⋯.measure = ⋯.measure + ∑ E : { x : Set (EuclideanSpace' d) // x ∈ S' }, ⋯.measure

Measure of a sum over insert a S' equals the measure of a plus the measure of the sum over S'.

theorem IsElementary.measure_of_disjUnion' {d : ℕ} {S : Finset (Set (EuclideanSpace' d))} (hE : ∀ E ∈ S, IsElementary E) (hdisj : (↑S).PairwiseDisjoint id) : ⋯.measure = ∑ E : { x : Set (EuclideanSpace' d) // x ∈ S }, ⋯.measure

Measure is additive on pairwise disjoint finsets of elementary sets.

@[simp]

theorem IsElementary.measure_of_empty (d : ℕ) : ⋯.measure = 0

The empty set has measure zero.

@[simp]

theorem IsElementary.measure_of_box {d : ℕ} (B : Box d) : ⋯.measure = B.volume

The measure of a single box equals its volume.

theorem IsElementary.measure_mono {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsElementary E) (hF : IsElementary F) (hcont : E ⊆ F) : hE.measure ≤ hF.measure

Elementary measure is monotone: if E ⊆ F then μ(E) ≤ μ(F).

theorem IsElementary.measure_of_union {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsElementary E) (hF : IsElementary F) : ⋯.measure ≤ hE.measure + hF.measure

Subadditivity of measure on unions: μ(E ∪ F) ≤ μ(E) + μ(F).

theorem IsElementary.measure_of_union' {d : ℕ} {S : Finset (Set (EuclideanSpace' d))} (hE : ∀ E ∈ S, IsElementary E) : ⋯.measure ≤ ∑ E : { x : Set (EuclideanSpace' d) // x ∈ S }, ⋯.measure

Subadditivity of measure on finset unions: μ(⋃ S) ≤ ∑ μ(E) for E ∈ S.

theorem BoundedInterval.length_of_translate (I : BoundedInterval) (c : ℝ) : ∃ (I' : BoundedInterval), ↑I' = ↑I + {c} ∧ I'.length = I.length

Helper: Translation preserves interval length

theorem Box.volume_of_translate {d : ℕ} (B : Box d) (x : EuclideanSpace' d) : ∃ (B' : Box d), ↑B' = ↑B + {x} ∧ B'.volume = B.volume

Helper: Translation preserves box volume

theorem Set.translate_inj {d : ℕ} (x : EuclideanSpace' d) (S₁ S₂ : Set (EuclideanSpace' d)) (h_eq : S₁ + {x} = S₂ + {x}) : S₁ = S₂

Translation is injective on sets: if S₁ + {x} = S₂ + {x}, then S₁ = S₂

theorem IsElementary.measure_of_translate {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : IsElementary E) (x : EuclideanSpace' d) : ⋯.measure = hE.measure

Elementary measure is translation-invariant: μ(E + {x}) = μ(E).

theorem IsElementary.measure_uniq {d : ℕ} {m' : (E : Set (EuclideanSpace' d)) → IsElementary E → ℝ} (hnonneg : ∀ (E : Set (EuclideanSpace' d)) (hE : IsElementary E), m' E hE ≥ 0) (hadd : ∀ (E F : Set (EuclideanSpace' d)) (hE : IsElementary E) (hF : IsElementary F), Disjoint E F → m' (E ∪ F) ⋯ = m' E hE + m' F hF) (htrans : ∀ (E : Set (EuclideanSpace' d)) (hE : IsElementary E) (x : EuclideanSpace' d), m' (E + {x}) ⋯ = m' E hE) : ∃ c ≥ 0, ∀ (E : Set (EuclideanSpace' d)) (hE : IsElementary E), m' E hE = c * hE.measure

Exercise 1.1.3 (uniqueness of elementary measure): Any non-negative, additive, translation-invariant function on elementary sets is a scalar multiple of the standard elementary measure.

@[reducible, inline]

abbrev Box.unit_cube (d : ℕ) : Box d

The d-dimensional unit cube (0,1]^d.

Equations

• Box.unit_cube d = { side := fun (x : Fin d) => BoundedInterval.Ioc 0 1 }

theorem IsElementary.measure_uniq' {d : ℕ} {m' : (E : Set (EuclideanSpace' d)) → IsElementary E → ℝ} (hnonneg : ∀ (E : Set (EuclideanSpace' d)) (hE : IsElementary E), m' E hE ≥ 0) (hadd : ∀ (E F : Set (EuclideanSpace' d)) (hE : IsElementary E) (hF : IsElementary F), Disjoint E F → m' (E ∪ F) ⋯ = m' E hE + m' F hF) (htrans : ∀ (E : Set (EuclideanSpace' d)) (hE : IsElementary E) (x : EuclideanSpace' d), m' (E + {x}) ⋯ = m' E hE) (hcube : m' ↑(Box.unit_cube d) ⋯ = 1) (E : Set (EuclideanSpace' d)) (hE : IsElementary E) : m' E hE = hE.measure

Any measure satisfying normalization m'(unit cube) = 1 must equal the standard elementary measure.

@[reducible, inline]

abbrev Box.prod {d₁ d₂ : ℕ} (B₁ : Box d₁) (B₂ : Box d₂) : Box (d₁ + d₂)

The Cartesian product of two boxes is a box in the sum dimension.

Equations

• B₁.prod B₂ = { side := fun (i : Fin (d₁ + d₂)) => Fin.casesOn i fun (i : ℕ) (hi : i < d₁ + d₂) => if h : i < d₁ then B₁.side ⟨i, h⟩ else B₂.side ⟨i - d₁, ⋯⟩ }

theorem IsElementary.prod {d₁ d₂ : ℕ} {E₁ : Set (EuclideanSpace' d₁)} {E₂ : Set (EuclideanSpace' d₂)} (hE₁ : IsElementary E₁) (hE₂ : IsElementary E₂) : IsElementary (EuclideanSpace'.prod E₁ E₂)

Exercise 1.1.4: The Cartesian product of two elementary sets is elementary.

theorem IsElementary.measure_of_prod {d₁ d₂ : ℕ} {E₁ : Set (EuclideanSpace' d₁)} {E₂ : Set (EuclideanSpace' d₂)} (hE₁ : IsElementary E₁) (hE₂ : IsElementary E₂) : ⋯.measure = hE₁.measure * hE₂.measure

Measure is multiplicative on products: μ(E₁ × E₂) = μ(E₁) * μ(E₂).