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

Визначення 1.1.1. (Intervals) We use the same formalization of intervals used in Chapter 11 of "Analysis I". Following the usual Lean preference to admit junk values, we allow for the possibility that b < a.

• 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) : ℝ

Визначення 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) : ℝ

Визначення 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)

Вправа 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)

Вправа 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)

Вправа 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)

Вправа 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})

Вправа 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

Лема 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)

Вправа 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))

Лема 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

Лема 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

Вправа 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

Вправа 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₂)

Вправа 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₂).