@[reducible, inline]

noncomputable abbrev Jordan_inner_measure {d : ℕ} (E : Set (EuclideanSpace' d)) : ℝ

Definition 1.1.4. We intend these concepts to only be applied for bounded sets E, but it is convenient to permit E to be unbounded for the purposes of making the definitions.

Equations

• Jordan_inner_measure E = sSup {m : ℝ | ∃ (A : Set (EuclideanSpace' d)) (hA : IsElementary A), A ⊆ E ∧ m = hA.measure}

@[reducible, inline]

noncomputable abbrev Jordan_outer_measure {d : ℕ} (E : Set (EuclideanSpace' d)) : ℝ

Equations

• Jordan_outer_measure E = sInf {m : ℝ | ∃ (A : Set (EuclideanSpace' d)) (hA : IsElementary A), E ⊆ A ∧ m = hA.measure}

@[reducible, inline]

noncomputable abbrev Jordan_inner_measure' {d : ℕ} (E : Set (EuclideanSpace' d)) : EReal

Definition 1.1.4, extended to unbounded sets. Exercise 1.2.5 of the text asks for the Jordan inner measure "extended to unbounded sets in the obvious manner". Because Jordan_inner_measure is real-valued, its supremum returns the junk value zero whenever the elementary subsets of a set have unbounded measure, as happens for the whole space; this variant takes the supremum in EReal instead, so that such a set receives the value infinity. The two agree on bounded sets, by Jordaninnermeasure'eqcoe below.

Equations

• Jordan_inner_measure' E = sSup {m : EReal | ∃ (A : Set (EuclideanSpace' d)) (hA : IsElementary A), A ⊆ E ∧ m = ↑hA.measure}

@[reducible, inline]

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

A bounded set is Jordan measurable if its inner and outer Jordan measures coincide.

Equations

• JordanMeasurable E = (Bornology.IsBounded E ∧ Jordan_inner_measure E = Jordan_outer_measure E)

@[reducible, inline]

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

The Jordan measure of a Jordan measurable set (equals both inner and outer measure).

Equations

• x✝.measure = Jordan_inner_measure E

theorem JordanMeasurable.eq_inner {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : JordanMeasurable E) : hE.measure = Jordan_inner_measure E

Jordan measure equals the inner Jordan measure by definition.

theorem JordanMeasurable.eq_outer {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : JordanMeasurable E) : hE.measure = Jordan_outer_measure E

For Jordan measurable sets, the measure also equals the outer Jordan measure.

theorem IsElementary.contains_bounded {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : ∃ (A : Set (EuclideanSpace' d)), IsElementary A ∧ E ⊆ A

Any bounded set is contained in some elementary set (a sufficiently large box).

theorem Jordan_inner_nonempty {d : ℕ} (E : Set (EuclideanSpace' d)) : {m : ℝ | ∃ (A : Set (EuclideanSpace' d)) (hA : IsElementary A), A ⊆ E ∧ m = hA.measure}.Nonempty

Every set has the empty set as an elementary subset, so the supremum defining the Jordan inner measure is taken over a nonempty set of reals.

theorem Jordan_inner_bddAbove {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : BddAbove {m : ℝ | ∃ (A : Set (EuclideanSpace' d)) (hA : IsElementary A), A ⊆ E ∧ m = hA.measure}

For a bounded set that supremum is also bounded above, by the measure of any elementary superset.

theorem EReal.sSup_image_coe {S : Set ℝ} (hne : S.Nonempty) (hbdd : BddAbove S) : sSup ((fun (x : ℝ) => ↑x) '' S) = ↑(sSup S)

For a nonempty set of reals that is bounded above, the supremum computed in EReal agrees with the supremum computed in the reals. Both hypotheses are needed: without them the real-valued supremum returns its junk value while the extended one returns an infinity.

theorem Jordan_inner_measure'_set_eq {d : ℕ} (E : Set (EuclideanSpace' d)) : {m : EReal | ∃ (A : Set (EuclideanSpace' d)) (hA : IsElementary A), A ⊆ E ∧ m = ↑hA.measure} = (fun (x : ℝ) => ↑x) '' {m : ℝ | ∃ (A : Set (EuclideanSpace' d)) (hA : IsElementary A), A ⊆ E ∧ m = hA.measure}

The extended-real and real descriptions of the elementary subset measures of a set are related by coercion.

theorem Jordan_inner_measure'_eq_coe {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : Jordan_inner_measure' E = ↑(Jordan_inner_measure E)

On bounded sets the extended Jordan inner measure agrees with Jordan_inner_measure, which is what makes it an extension of Definition 1.1.4 rather than a different notion.

theorem Jordan_inner_measure'_univ {d : ℕ} (hd : 0 < d) : Jordan_inner_measure' Set.univ = ⊤

The extended Jordan inner measure of the whole space is infinite in positive dimension, which is the behaviour the text intends when it extends the definition to unbounded sets. By contrast Jordan_inner_measure returns its junk value of zero here, because it takes a supremum in the reals over a set with no upper bound. This is why Exercise 1.2.5 and the formula for the outer measure of an open set have to be stated with the extended version.

theorem EuclideanSpace'.isBounded_of_dim_zero (E : Set (EuclideanSpace' 0)) : Bornology.IsBounded E

In dimension zero the whole space is a single point, so every set is bounded.

theorem Jordan_inner_measure_nonneg {d : ℕ} (E : Set (EuclideanSpace' d)) : 0 ≤ Jordan_inner_measure E

The inner Jordan measure is always non-negative.

theorem Jordan_outer_measure_nonneg {d : ℕ} (E : Set (EuclideanSpace' d)) : 0 ≤ Jordan_outer_measure E

The outer Jordan measure is always non-negative.

theorem Jordan_inner_le_outer {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : Jordan_inner_measure E ≤ Jordan_outer_measure E

For bounded sets, inner Jordan measure is at most outer Jordan measure.

theorem le_Jordan_inner {d : ℕ} {E A : Set (EuclideanSpace' d)} (hA : IsElementary A) (hAE : A ⊆ E) (hE : Bornology.IsBounded E) : hA.measure ≤ Jordan_inner_measure E

Elementary measure of a subset is a lower bound for inner Jordan measure.

theorem le_Jordan_inner_self {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) : hA.measure ≤ Jordan_inner_measure A

The elementary measure of a set is a lower bound for its own inner Jordan measure.

theorem Jordan_outer_le {d : ℕ} {E A : Set (EuclideanSpace' d)} (hA : IsElementary A) (hAE : E ⊆ A) : Jordan_outer_measure E ≤ hA.measure

Elementary measure of a superset is an upper bound for outer Jordan measure.

theorem Jordan_outer_le_self {d : ℕ} {A : Set (EuclideanSpace' d)} (hA : IsElementary A) : Jordan_outer_measure A ≤ hA.measure

The elementary measure of a set is an upper bound for its own outer Jordan measure.

theorem Jordan_inner_le {d : ℕ} {E : Set (EuclideanSpace' d)} {m : ℝ} (hm : m < Jordan_inner_measure E) : ∃ (A : Set (EuclideanSpace' d)) (hA : IsElementary A), A ⊆ E ∧ m < hA.measure

If m < inner measure, there exists an elementary subset with measure > m.

theorem le_Jordan_outer {d : ℕ} {E : Set (EuclideanSpace' d)} {m : ℝ} (hm : Jordan_outer_measure E < m) (hbound : Bornology.IsBounded E) : ∃ (A : Set (EuclideanSpace' d)) (hA : IsElementary A), E ⊆ A ∧ hA.measure < m

If outer measure < m, there exists an elementary superset with measure < m.

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

An elementary set is bounded: it is a finite union of boxes, and each box sits inside the closed ball of radius the norm of its corner.

theorem JordanMeasurable.equiv {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : [JordanMeasurable E, ∀ ε > 0, ∃ (A : Set (EuclideanSpace' d)) (B : Set (EuclideanSpace' d)) (hA : IsElementary A) (hB : IsElementary B), A ⊆ E ∧ E ⊆ B ∧ ⋯.measure ≤ ε, ∀ ε > 0, ∃ (A : Set (EuclideanSpace' d)) (_ : IsElementary A), Jordan_outer_measure (_root_.symmDiff E A) ≤ ε].TFAE

Exercise 1.1.5

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

Every elementary set is Jordan measurable.

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

The Jordan measure of an elementary set equals its elementary measure.

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

The empty set is Jordan measurable.

@[simp]

theorem JordanMeasurable.mes_of_empty (d : ℕ) : ⋯.measure = 0

The empty set has Jordan measure zero.

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

Exercise 1.1.6 (i) (Boolean closure)

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

The union of a finset of Jordan measurable sets is Jordan measurable.

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

Exercise 1.1.6 (i) (Boolean closure)

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

Exercise 1.1.6 (i) (Boolean closure)

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

Exercise 1.1.6 (i) (Boolean closure)

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

Exercise 1.1.6 (ii) (non-negativity)

theorem Jordan_inner_add_le {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) (hF : Bornology.IsBounded F) (hdisj : Disjoint E F) : Jordan_inner_measure E + Jordan_inner_measure F ≤ Jordan_inner_measure (E ∪ F)

theorem Jordan_outer_subadd {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) (hF : Bornology.IsBounded F) : Jordan_outer_measure (E ∪ F) ≤ Jordan_outer_measure E + Jordan_outer_measure F

theorem JordanMeasurable.mes_of_disjUnion {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : JordanMeasurable E) (hF : JordanMeasurable F) (hEF : Disjoint E F) : ⋯.measure = hE.measure + hF.measure

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

Exercise 1.1.6 (iii) (finite additivity)

theorem JordanMeasurable.mono {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : JordanMeasurable E) (hF : JordanMeasurable F) (hEF : E ⊆ F) : hE.measure ≤ hF.measure

Exercise 1.1.6 (iv) (monotonicity)

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

Exercise 1.1.6 (v) (finite subadditivity)

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

Exercise 1.1.6 (v) (finite subadditivity)

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

Exercise 1.1.6 (vi) (translation invariance)

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

Exercise 1.1.6 (vi) (translation invariance)

theorem JordanMeasurable.graph {d : ℕ} {B : Box d} (hB : IsClosed ↑B) {f : EuclideanSpace' d → ℝ} (hf : ContinuousOn f ↑B) : JordanMeasurable {p : EuclideanSpace' (d + 1) | ∃ x ∈ ↑B, (EuclideanSpace'.prod_equiv d 1) p = (x, Real.equiv_EuclideanSpace' (f x))}

Exercise 1.1.7 (i) (Regions under graphs are Jordan measurable)

theorem JordanMeasurable.measure_of_graph {d : ℕ} {B : Box d} (hB : IsClosed ↑B) {f : EuclideanSpace' d → ℝ} (hf : ContinuousOn f ↑B) : ⋯.measure = 0

Exercise 1.1.7 (i) (Regions under graphs are Jordan measurable)

theorem JordanMeasurable.undergraph {d : ℕ} {B : Box d} (hB : IsClosed ↑B) {f : EuclideanSpace' d → ℝ} (hf : ContinuousOn f ↑B) : JordanMeasurable {p : EuclideanSpace' (d + 1) | ∃ x ∈ ↑B, ∃ (t : ℝ), (EuclideanSpace'.prod_equiv d 1) p = (x, Real.equiv_EuclideanSpace' t) ∧ 0 ≤ t ∧ t ≤ f x}

Exercise 1.1.7 (i) (Regions under graphs are Jordan measurable)

theorem JordanMeasurable.triangle (T : Affine.Triangle ℝ (EuclideanSpace' 2)) : JordanMeasurable (Affine.Simplex.closedInterior T)

Exercise 1.1.8(i) (A triangle is Jordan measurable)

@[reducible, inline]

abbrev EuclideanSpace'.plane_wedge (x y : EuclideanSpace' 2) : (fun (x : Fin 2) => ℝ) 1

The 2D wedge product (signed area parallelogram factor) of two vectors.

Equations

• x.plane_wedge y = x.ofLp 1 * y.ofLp 0 - x.ofLp 0 * y.ofLp 1

theorem JordanMeasurable.measure_triangle (T : Affine.Triangle ℝ (EuclideanSpace' 2)) : ⋯.measure = |(T.points 1 - T.points 0).plane_wedge (T.points 2 - T.points 0)| / 2

Exercise 1.1.8(ii) (Jordan measure of a triangle)

@[reducible, inline]

abbrev IsPolytope {d : ℕ} (P : Set (EuclideanSpace' d)) : Prop

Exercise 1.1.9 A polytope is the convex hull of a finite set of vertices.

Equations

• IsPolytope P = ∃ (V : Finset (EuclideanSpace' d)), P = (convexHull ℝ) ↑V

theorem JordanMeasurable.polytope {d : ℕ} {P : Set (EuclideanSpace' d)} (hP : IsPolytope P) : JordanMeasurable P

Exercise 1.1.9: Every polytope is Jordan measurable.

theorem JordanMeasurable.ball {d : ℕ} (x₀ : EuclideanSpace' d) {r : ℝ} (hr : 0 < r) : JordanMeasurable (Metric.ball x₀ r)

Exercise 1.1.10 (1)

theorem JordanMeasurable.closedBall {d : ℕ} (x₀ : EuclideanSpace' d) {r : ℝ} (hr : 0 < r) : JordanMeasurable (Metric.closedBall x₀ r)

Exercise 1.1.10 (1)

theorem JordanMeasurable.measure_ball (d : ℕ) : ∃ (c : ℝ), ∀ (x₀ : EuclideanSpace' d) (r : ℝ) (hr : 0 < r), ⋯.measure = c * r ^ d

Exercise 1.1.10 (1)

theorem JordanMeasurable.measure_closedBall {d : ℕ} (x₀ : EuclideanSpace' d) {r : ℝ} (hr : 0 < r) : ⋯.measure = ⋯.measure

The Jordan measure of a closed ball equals that of the open ball.

theorem JordanMeasurable.measure_ball_le (d : ℕ) : ⋯.choose ≤ 2 ^ d

Exercise 1.1.10 (2)

theorem JordanMeasurable.le_measure_ball (d : ℕ) : 2 ^ d / ↑d.factorial ≤ ⋯.choose

Exercise 1.1.10 (2)

theorem JordanMeasurable.linear_of_elem {d : ℕ} (T : EuclideanSpace' d ≃ₗ[ℝ] EuclideanSpace' d) {E : Set (EuclideanSpace' d)} (hE : IsElementary E) : JordanMeasurable (⇑T '' E)

Exercise 1.1.11 (1)

theorem JordanMeasurable.measure_linear_of_elem {d : ℕ} (T : EuclideanSpace' d ≃ₗ[ℝ] EuclideanSpace' d) : ∃ D > 0, ∀ (E : Set (EuclideanSpace' d)) (hE : IsElementary E), ⋯.measure = D * hE.measure

Exercise 1.1.11 (1)

theorem JordanMeasurable.linear {d : ℕ} (T : EuclideanSpace' d ≃ₗ[ℝ] EuclideanSpace' d) {E : Set (EuclideanSpace' d)} (hE : JordanMeasurable E) : JordanMeasurable (⇑T '' E)

Exercise 1.1.11 (2)

theorem JordanMeasurable.measure_linear {d : ℕ} (T : EuclideanSpace' d ≃ₗ[ℝ] EuclideanSpace' d) : ∃ D > 0, ∀ (E : Set (EuclideanSpace' d)) (hE : JordanMeasurable E), ⋯.measure = D * hE.measure

Exercise 1.1.11 (2)

noncomputable def Matrix.linear_equiv {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) [Invertible A] : EuclideanSpace' d ≃ₗ[ℝ] EuclideanSpace' d

An invertible matrix defines a linear equivalence on Euclidean space.

Equations

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

theorem JordanMeasurable.measure_linear_det {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) [Invertible A] : ⋯.choose = |A.det|

Exercise 1.1.11 (3)

@[reducible, inline]

abbrev JordanMeasurable.null {d : ℕ} (E : Set (EuclideanSpace' d)) : Prop

A set is Jordan null if it is Jordan measurable with measure zero.

Equations

• JordanMeasurable.null E = ∃ (hE : JordanMeasurable E), hE.measure = 0

theorem JordanMeasurable.null_iff {d : ℕ} {E : Set (EuclideanSpace' d)} : null E ↔ Bornology.IsBounded E ∧ Jordan_outer_measure E = 0

A set is Jordan null iff it's bounded with outer Jordan measure zero.

theorem JordanMeasurable.null_mono {d : ℕ} {E F : Set (EuclideanSpace' d)} (h : null E) (hEF : F ⊆ E) : null F

Exercise 1.1.12

theorem JordanMeasure.measure_eq {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : JordanMeasurable E) : Filter.Tendsto (fun (N : ℕ) => ↑N ^ (-↑d) * ↑(Nat.card ↑(E ∩ Set.range fun (n : Fin d → ℤ) => WithLp.toLp 2 fun (i : Fin d) => (↑N)⁻¹ * ↑(n i)))) Filter.atTop (nhds hE.measure)

Exercise 1.1.13

@[reducible, inline]

noncomputable abbrev Box.dyadic {d : ℕ} (n : ℤ) (i : Fin d → ℤ) : Box d

A dyadic box at scale 2^(-n) with multi-index i: the half-open cube [i/2^n, (i+1)/2^n).

Equations

• Box.dyadic n i = { side := fun (j : Fin d) => BoundedInterval.Ico (↑(i j) / 2 ^ n) ((↑(i j) + 1) / 2 ^ n) }

@[reducible, inline]

noncomputable abbrev metric_entropy_lower {d : ℕ} (E : Set (EuclideanSpace' d)) (n : ℤ) : ℕ

Lower metric entropy: count of dyadic boxes at scale n fully contained in E.

Equations

• metric_entropy_lower E n = Nat.card ↑{i : Fin d → ℤ | ↑(Box.dyadic n i) ⊆ E}

@[reducible, inline]

noncomputable abbrev metric_entropy_upper {d : ℕ} (E : Set (EuclideanSpace' d)) (n : ℤ) : ℕ

Upper metric entropy: count of dyadic boxes at scale n that intersect E.

Equations

• metric_entropy_upper E n = Nat.card ↑{i : Fin d → ℤ | ↑(Box.dyadic n i) ∩ E ≠ ∅}

theorem JordanMeasure.iff {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : JordanMeasurable E ↔ Filter.Tendsto (fun (n : ℤ) => 2 ^ (-(↑d * n)) * (↑(metric_entropy_upper E n) - ↑(metric_entropy_lower E n))) Filter.atTop (nhds 0)

Exercise 1.1.14

theorem JordanMeasure.eq_lim_lower {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : JordanMeasurable E) : Filter.Tendsto (fun (n : ℤ) => 2 ^ (-(↑d * n)) * ↑(metric_entropy_lower E n)) Filter.atTop (nhds hE.measure)

Jordan measure equals the limit of scaled lower metric entropy.

theorem JordanMeasure.eq_lim_upper {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : JordanMeasurable E) : Filter.Tendsto (fun (n : ℤ) => 2 ^ (-(↑d * n)) * ↑(metric_entropy_upper E n)) Filter.atTop (nhds hE.measure)

Jordan measure equals the limit of scaled upper metric entropy.

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

Exercise 1.1.15 (Uniqueness of Jordan measure)

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

With unit cube normalization, the unique such function equals Jordan measure.

theorem EuclideanSpace'.norm_prod_equiv_symm {d₁ d₂ : ℕ} (y : EuclideanSpace' d₁) (z : EuclideanSpace' d₂) : ‖(prod_equiv d₁ d₂).symm (y, z)‖ ^ 2 = ‖y‖ ^ 2 + ‖z‖ ^ 2

The Cartesian product of bounded sets is bounded.

theorem EuclideanSpace'.prod_mono {d₁ d₂ : ℕ} {E₁ E₁' : Set (EuclideanSpace' d₁)} {E₂ E₂' : Set (EuclideanSpace' d₂)} (h₁ : E₁ ⊆ E₁') (h₂ : E₂ ⊆ E₂') : prod E₁ E₂ ⊆ prod E₁' E₂'

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

theorem Jordan_outer_measure_prod_le {d₁ d₂ : ℕ} {E₁ : Set (EuclideanSpace' d₁)} {E₂ : Set (EuclideanSpace' d₂)} (hE₁ : JordanMeasurable E₁) (hE₂ : JordanMeasurable E₂) : Jordan_outer_measure (EuclideanSpace'.prod E₁ E₂) ≤ hE₁.measure * hE₂.measure

Outer Jordan measure of a product is at most the product of the measures.

theorem Jordan_inner_measure_prod_ge {d₁ d₂ : ℕ} {E₁ : Set (EuclideanSpace' d₁)} {E₂ : Set (EuclideanSpace' d₂)} (hE₁ : JordanMeasurable E₁) (hE₂ : JordanMeasurable E₂) : hE₁.measure * hE₂.measure ≤ Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂)

Inner Jordan measure of a product is at least the product of the measures.

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

Exercise 1.1.16

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

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

@[reducible, inline]

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

Two sets are isometric if one is an orthogonal transformation plus translation of the other.

Equations

• Isometric E F = ∃ A ∈ Matrix.orthogonalGroup (Fin d) ℝ, ∃ (x₀ : EuclideanSpace' d), F = (fun (x : EuclideanSpace' d) => WithLp.toLp 2 ((Matrix.toLin' A) x.ofLp)) '' E + {x₀}

theorem JordanMeasurable.measure_of_equidecomposable {d n : ℕ} {E F : Set (EuclideanSpace' d)} (hE : JordanMeasurable E) (hF : JordanMeasurable F) {P Q : Fin n → Set (EuclideanSpace' d)} (hPQ : ∀ (i : Fin n), Isometric (P i) (Q i)) (hPE : E = ⋃ (i : Fin n), P i) (hQF : F = ⋃ (i : Fin n), Q i) (hPdisj : Set.univ.PairwiseDisjoint P) (hQdisj : Set.univ.PairwiseDisjoint fun (i : Fin n) => interior (Q i)) : hE.measure = hF.measure

Exercise 1.1.17

theorem JordanMeasurable.outer_measure_of_closure {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : Jordan_outer_measure (closure E) = Jordan_outer_measure E

Exercise 1.1.18 (1)

theorem JordanMeasurable.inner_measure_of_interior {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : Jordan_inner_measure (interior E) = Jordan_inner_measure E

Exercise 1.1.18 (2)

theorem JordanMeasurable.iff_boundary_null {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) : JordanMeasurable E ↔ null (frontier E)

Exercise 1.1.18 (3)

@[reducible, inline]

abbrev bullet_riddled_square : Set (EuclideanSpace' 2)

The unit square with all rational points removed (not Jordan measurable).

Equations

• bullet_riddled_square = {x : EuclideanSpace' 2 | ∀ (i : Fin 2), x.ofLp i ∈ Set.Icc 0 1 ∧ x.ofLp i ∉ (fun (q : ℚ) => ↑q) '' Set.univ}

@[reducible, inline]

abbrev bullets : Set (EuclideanSpace' 2)

The set of rational points in the unit square (not Jordan measurable).

Equations

• bullets = {x : EuclideanSpace' 2 | ∀ (i : Fin 2), x.ofLp i ∈ Set.Icc 0 1 ∧ x.ofLp i ∈ (fun (q : ℚ) => ↑q) '' Set.univ}

theorem bullet_riddled_square.inner : Jordan_inner_measure bullet_riddled_square = 0

The bullet-riddled square has inner Jordan measure 0 (no elementary subset).

theorem bullet_riddled_square.outer : Jordan_outer_measure bullet_riddled_square = 1

The bullet-riddled square has outer Jordan measure 1 (fills the unit square).

theorem bullets.inner : Jordan_inner_measure bullets = 0

The rational points in the unit square have inner Jordan measure 0.

theorem bullets.outer : Jordan_outer_measure bullets = 1

The rational points in the unit square have outer Jordan measure 1.

theorem bullet_riddled_square.not_jordanMeasurable : ¬JordanMeasurable bullet_riddled_square

The bullet-riddled square is not Jordan measurable (inner ≠ outer).

theorem bullets.not_jordanMeasurable : ¬JordanMeasurable bullets

The set of rational points is not Jordan measurable (inner ≠ outer).

theorem JordanMeasurable.caratheodory {d : ℕ} {E F : Set (EuclideanSpace' d)} (hE : Bornology.IsBounded E) (hF : IsElementary F) : Jordan_outer_measure E = Jordan_outer_measure (E ∩ F) + Jordan_outer_measure (E \ F)

Exercise 1.1.19 (Caratheodory property)