Introduction to Measure Theory, Section 1.1.2: Jordan measure

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

@[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 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_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) : hA.measure ≤ Jordan_inner_measure A

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

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

Elementary measure of a superset is an upper bound for 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 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 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

Exercise 1.1.6 (iii) (finite additivity)

theorem JordanMeasurable.measure_of_disjUnion' {d : ℕ} {S : Finset (Set (EuclideanSpace' d))} (hE : ∀ E ∈ S, JordanMeasurable E) (hdisj : (↑S).PairwiseDisjoint id) : ⋯.measure = ∑ E : { x : Set (EuclideanSpace' d) // x ∈ 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 : { x : Set (EuclideanSpace' d) // x ∈ 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} {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} {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} {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

@[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 1 * y 0 - x 0 * y 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

@[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 = 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 → ℤ) (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 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 = ⇑(Matrix.toLin' A) '' 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 i ∈ Set.Icc 0 1 ∧ x 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 i ∈ Set.Icc 0 1 ∧ x 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)