Analysis.MeasureTheory.Section_1_1

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

source

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.

source

theorem BoundedInterval.inter (I J : BoundedInterval) :

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

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

source

@[implicit_reducible]

noncomputable instance BoundedInterval.instInter :

Inter BoundedInterval

Instance enabling ∩ notation for BoundedIntervals.

Equations

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

source

@[simp]

theorem BoundedInterval.inter_eq (I J : BoundedInterval) :

↑(I ∩ J) = ↑I ∩ ↑J

The intersection of BoundedIntervals equals the set-theoretic intersection.

source

@[implicit_reducible]

instance BoundedInterval.instMembership :

Membership ℝ BoundedInterval

Instance enabling ∈ notation for membership in BoundedInterval.

Equations

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

source

@[simp]

theorem BoundedInterval.mem_iff (I : BoundedInterval) (x : ℝ) :

x ∈ I ↔ x ∈ ↑I

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

source

@[implicit_reducible]

instance BoundedInterval.instSubset :

HasSubset BoundedInterval

Instance enabling ⊆ notation for BoundedIntervals.

Equations

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

source

@[simp]

theorem BoundedInterval.subset_iff (I J : BoundedInterval) :

I ⊆ J ↔ ↑I ⊆ ↑J

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

source

@[reducible, inline]

abbrev BoundedInterval.a (I : BoundedInterval) :

ℝ

Extracts the left endpoint of a bounded interval.

Equations

Instances For

source

@[reducible, inline]

abbrev BoundedInterval.b (I : BoundedInterval) :

ℝ

Extracts the right endpoint of a bounded interval.

Equations

Instances For

source

theorem BoundedInterval.nonempty_implies_le (I : BoundedInterval) (h : (↑I).Nonempty) :

I.a ≤ I.b

Any nonempty BoundedInterval has a ≤ b

source

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.

source

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.

source

@[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

Instances For

source

theorem BoundedInterval.length_nonneg (I : BoundedInterval) :

0 ≤ I.length

Length is always non-negative

source

def «term|___|ₗ» :

Lean.ParserDescr

Using ||ₗ subscript here to not override ||

Equations

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

Instances For

source

structure Box (d : ℕ) :

Type

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

side : Fin d → BoundedInterval

Instances For

source

theorem Box.ext_iff {d : ℕ} {x y : Box d} :

x = y ↔ x.side = y.side

source

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

x = y

source

def Box.toSet {d : ℕ} (B : Box d) :

Set (EuclideanSpace' d)

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

Equations

↑B = {x : EuclideanSpace' d | ∀ (i : Fin d), x.ofLp i ∈ ↑(B.side i)}

Instances For

source

@[simp]

theorem Box.mem_toSet {d : ℕ} {B : Box d} {x : EuclideanSpace' d} :

x ∈ ↑B ↔ ∀ (i : Fin d), x.ofLp i ∈ ↑(B.side i)

source

@[implicit_reducible]

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 }

source

@[implicit_reducible]

noncomputable instance Box.decidableEq {d : ℕ} :

DecidableEq (Box d)

This is to make Finsets of Boxes work properly.

Equations

a.decidableEq b = decidable_of_iff (a.side = b.side) ⋯

source

@[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 }

Instances For

source

@[implicit_reducible]

instance BoundedInterval.inst_coeBox :

Coe BoundedInterval (Box 1)

Enables coercion from BoundedInterval to Box 1.

Equations

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

source

@[simp]

theorem BoundedInterval.toBox_inj {I J : BoundedInterval} :

↑I = ↑J ↔ I = J

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

source

@[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.

source

@[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

Instances For

source

def «term|___|ᵥ» :

Lean.ParserDescr

Using ||ᵥ subscript here to not override ||

Equations

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

Instances For

source

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

source

theorem Box.volume_singleton {d : ℕ} (hd : 0 < d) (x : EuclideanSpace' d) :

{ side := fun (i : Fin d) => BoundedInterval.Icc (x.ofLp i) (x.ofLp i) }.volume = 0

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

source

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

source

@[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.

source

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

source

@[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

Instances For

source

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

IsElementary ↑B

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

source

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.

source

theorem IsElementary.empty (d : ℕ) :

IsElementary ∅

The empty set is elementary.

source

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.

source

theorem Box.inter {d : ℕ} (B₁ B₂ : Box d) :

∃ (B : Box d), ↑B = ↑B₁ ∩ ↑B₂

The intersection of two boxes is a box: intersect the sides coordinatewise.

source

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.

source

def BoundedInterval.mk' (a b : ℝ) (lclosed uclosed : Bool) :

BoundedInterval

The bounded interval with the given endpoints, open or closed at each end as specified.

Equations

BoundedInterval.mk' a b true true = BoundedInterval.Icc a b
BoundedInterval.mk' a b true false = BoundedInterval.Ico a b
BoundedInterval.mk' a b false true = BoundedInterval.Ioc a b
BoundedInterval.mk' a b false false = BoundedInterval.Ioo a b

Instances For

source

def BoundedInterval.lclosed :

BoundedInterval → Bool

Whether a bounded interval contains its left endpoint.

Equations

(BoundedInterval.Icc a b).lclosed = true
(BoundedInterval.Ico a b).lclosed = true
(BoundedInterval.Ioo a b).lclosed = false
(BoundedInterval.Ioc a b).lclosed = false

Instances For

source

def BoundedInterval.uclosed :

BoundedInterval → Bool

Whether a bounded interval contains its right endpoint.

Equations

(BoundedInterval.Icc a b).uclosed = true
(BoundedInterval.Ioc a b).uclosed = true
(BoundedInterval.Ioo a b).uclosed = false
(BoundedInterval.Ico a b).uclosed = false

Instances For

source

@[simp]

theorem BoundedInterval.mk'_a (a b : ℝ) (lclosed uclosed : Bool) :

(mk' a b lclosed uclosed).a = a

source

@[simp]

theorem BoundedInterval.mk'_b (a b : ℝ) (lclosed uclosed : Bool) :

(mk' a b lclosed uclosed).b = b

source

@[simp]

theorem BoundedInterval.mk'_lclosed (a b : ℝ) (lclosed uclosed : Bool) :

(mk' a b lclosed uclosed).lclosed = lclosed

source

@[simp]

theorem BoundedInterval.mk'_uclosed (a b : ℝ) (lclosed uclosed : Bool) :

(mk' a b lclosed uclosed).uclosed = uclosed

source

theorem BoundedInterval.mem_iff' (I : BoundedInterval) (x : ℝ) :

x ∈ ↑I ↔ (if I.lclosed = true then I.a ≤ x else I.a < x) ∧ if I.uclosed = true then x ≤ I.b else x < I.b

source

theorem BoundedInterval.sdiff (I J : BoundedInterval) :

∃ (K₁ : BoundedInterval) (K₂ : BoundedInterval), ↑I \ ↑J = ↑K₁ ∪ ↑K₂

The set difference of two bounded intervals is the union of two bounded intervals: the part of the first below the second, and the part above it.

source

theorem Box.sdiff {d : ℕ} (B C : Box d) :

IsElementary (↑B \ ↑C)

The difference of two boxes is elementary: a point of the difference leaves the second box in some coordinate, and in that coordinate the difference of the two sides is a union of two intervals.

source

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.

source

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.

source

theorem BoundedInterval.translate (I : BoundedInterval) (c : ℝ) :

↑(mk' (I.a + c) (I.b + c) I.lclosed I.uclosed) = ↑I + {c}

Translating a bounded interval gives a bounded interval with the same open/closed ends.

source

theorem Box.translate {d : ℕ} (B : Box d) (x : EuclideanSpace' d) :

∃ (B' : Box d), ↑B' = ↑B + {x}

Translating a box gives a box.

source

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.

source

theorem BoundedInterval.partition (S : Finset BoundedInterval) :

∃ (T : Finset BoundedInterval), (↑T).PairwiseDisjoint toSet ∧ ∀ I ∈ S, ∃ (U : Set ↥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.

source

theorem Box.partition {d : ℕ} (S : Finset (Box d)) :

∃ (T : Finset (Box d)), (↑T).PairwiseDisjoint toSet ∧ ∀ I ∈ S, ∃ (U : Set ↥T), ↑I = ⋃ J ∈ U, ↑↑J

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

source

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.

source

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.

source

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.

source

def Box.sample_congr {d : ℕ} (B : Box d) (N : ℕ) :

↑(↑B ∩ Set.range fun (n : Fin d → ℤ) => WithLp.toLp 2 fun (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.

Instances For

source

theorem Box.sample_finite {d : ℕ} (B : Box d) {N : ℕ} (hN : N ≠ 0) :

Finite ↑(↑B ∩ Set.range fun (n : Fin d → ℤ) => WithLp.toLp 2 fun (i : Fin d) => (↑N)⁻¹ * ↑(n i))

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

source

theorem Box.vol_eq {d : ℕ} (B : Box d) :

Filter.Tendsto (fun (N : ℕ) => ↑N ^ (-↑d) * ↑(Nat.card ↑(↑B ∩ Set.range fun (n : Fin d → ℤ) => WithLp.toLp 2 fun (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).

source

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 → ℤ) => WithLp.toLp 2 fun (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.

source

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.

source

@[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

Instances For

source

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.

source

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.

source

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

0 ≤ hE.measure

Elementary measure is always non-negative.

source

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).

source

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.

source

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.

source

theorem IsElementary.union'_empty_eq {d : ℕ} :

⋃ E ∈ ∅, E = ∅

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

source

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 : ↥(insert a S'), ⋯.measure = ⋯.measure + ∑ E : ↥S', ⋯.measure

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

source

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

⋯.measure = ∑ E : ↥S, ⋯.measure

Measure is additive on pairwise disjoint finsets of elementary sets.

source

@[simp]

theorem IsElementary.measure_of_empty (d : ℕ) :

⋯.measure = 0

The empty set has measure zero.

source

@[simp]

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

⋯.measure = B.volume

The measure of a single box equals its volume.

source

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).

source

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).

source

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

⋯.measure ≤ ∑ E : ↥S, ⋯.measure

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

source

theorem BoundedInterval.length_of_translate (I : BoundedInterval) (c : ℝ) :

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

Helper: Translation preserves interval length

source

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

source

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₂

source

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).

source

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.

source

@[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 }

Instances For

source

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.

source

@[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₁, ⋯⟩ }

Instances For

source

theorem Box.prod_side {d₁ d₂ : ℕ} (B₁ : Box d₁) (B₂ : Box d₂) (i : Fin (d₁ + d₂)) :

(B₁.prod B₂).side i = if h : ↑i < d₁ then B₁.side ⟨↑i, h⟩ else B₂.side ⟨↑i - d₁, ⋯⟩

Unfold Box.prod on a coordinate.

source

theorem EuclideanSpace'.prod_equiv_symm_apply_left {d₁ d₂ : ℕ} (y : EuclideanSpace' d₁) (z : EuclideanSpace' d₂) {i : ℕ} (hi : i < d₁) :

((prod_equiv d₁ d₂).symm (y, z)).ofLp ⟨i, ⋯⟩ = y.ofLp ⟨i, hi⟩

Coordinate of a product vector in the first block.

source

theorem EuclideanSpace'.prod_equiv_symm_apply_right {d₁ d₂ : ℕ} (y : EuclideanSpace' d₁) (z : EuclideanSpace' d₂) {j : ℕ} (hj : j < d₂) :

((prod_equiv d₁ d₂).symm (y, z)).ofLp ⟨d₁ + j, ⋯⟩ = z.ofLp ⟨j, hj⟩

Coordinate of a product vector in the second block.

source

theorem EuclideanSpace'.prod_equiv_apply_fst {d₁ d₂ : ℕ} (x : EuclideanSpace' (d₁ + d₂)) (i : Fin d₁) :

((prod_equiv d₁ d₂) x).1.ofLp i = x.ofLp ⟨↑i, ⋯⟩

First factor of prod_equiv.

source

theorem EuclideanSpace'.prod_equiv_apply_snd {d₁ d₂ : ℕ} (x : EuclideanSpace' (d₁ + d₂)) (j : Fin d₂) :

((prod_equiv d₁ d₂) x).2.ofLp j = x.ofLp ⟨↑j + d₁, ⋯⟩

Second factor of prod_equiv. Matches toFun, which uses i + d₁.

source

theorem Box.prod_toSet {d₁ d₂ : ℕ} (B₁ : Box d₁) (B₂ : Box d₂) :

EuclideanSpace'.prod ↑B₁ ↑B₂ = ↑(B₁.prod B₂)

The set of a product box is the Cartesian product of the two boxes.

source

theorem Box.prod_injective {d₁ d₂ : ℕ} :

Function.Injective fun (p : Box d₁ × Box d₂) => p.1.prod p.2

Recovering the factors from a product box.

source

theorem Box.volume_prod {d₁ d₂ : ℕ} (B₁ : Box d₁) (B₂ : Box d₂) :

(B₁.prod B₂).volume = B₁.volume * B₂.volume

Volume of a product box is the product of the volumes.

source

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.

source

theorem Box.prod_pairwiseDisjoint {d₁ d₂ : ℕ} {S : Finset (Box d₁)} {T : Finset (Box d₂)} (hS : (↑S).PairwiseDisjoint toSet) (hT : (↑T).PairwiseDisjoint toSet) :

(↑(Finset.image (fun (p : Box d₁ × Box d₂) => p.1.prod p.2) (S ×ˢ T))).PairwiseDisjoint toSet

The product of two pairwise disjoint box families remains pairwise disjoint.

source

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₂).

Documentation

Analysis.MeasureTheory.Section_1_1_1