Introduction to Measure Theory, Section 1.3.2: Measurable functions

A companion to (the introduction to) Section 1.3.2 of the book "An introduction to Measure Theory".

def Unsigned {X : Type u_1} {Y : Type u_2} [LE Y] [Zero Y] (f : X → Y) : Prop

Equations

• Unsigned f = ∀ (x : X), f x ≥ 0

def PointwiseConvergesTo {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] (f : ℕ → X → Y) (g : X → Y) : Prop

Equations

• PointwiseConvergesTo f g = ∀ (x : X), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))

def UnsignedMeasurable {d : ℕ} (f : EuclideanSpace' d → EReal) : Prop

Definiiton 1.3.8 (Unsigned measurable function)

Equations

• UnsignedMeasurable f = (Unsigned f ∧ ∃ (g : ℕ → EuclideanSpace' d → EReal), (∀ (n : ℕ), UnsignedSimpleFunction (g n)) ∧ PointwiseConvergesTo g f)

def EReal.BoundedFunction {X : Type u_1} (f : X → EReal) : Prop

Equations

• EReal.BoundedFunction f = ∃ (M : NNReal), ∀ (x : X), (f x).abs ≤ ↑M

def FiniteMeasureSupport {d : ℕ} {Y : Type u_1} [Zero Y] (f : EuclideanSpace' d → Y) : Prop

Equations

• FiniteMeasureSupport f = (Lebesgue_measure (Support f) < ⊤)

def PointwiseAeConvergesTo {d : ℕ} {Y : Type u_1} [TopologicalSpace Y] (f : ℕ → EuclideanSpace' d → Y) (g : EuclideanSpace' d → Y) : Prop

Equations

• PointwiseAeConvergesTo f g = AlmostAlways fun (x : EuclideanSpace' d) => Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))

Helper lemmas for Lemma 1.3.9

The proof follows the book's implication chain. We establish explicit edges and let tfae_finish compute the transitive closure.

Explicit edges declared:

• (i) ⟺ (ii): by definition of UnsignedMeasurable
• (ii) ⟹ (iii): pointwise everywhere implies pointwise a.e.
• (iv) ⟹ (ii): monotone sequences in [0,∞] converge to their supremum
• (iii) ⟹ (v): via limsup representation (main technical work)
• (v) ⟺ (vi): countable unions/intersections
• (vi) ⟺ (vii): complementation
• (v) ⟺ (viii): complementation
• (v)-(viii) ⟹ (ix): intervals are intersections of half-intervals
• (ix) ⟹ (x): open sets are countable unions of intervals
• (x) ⟺ (xi): complementation
• (x) ⟹ (vii): {f < λ} = f⁻¹'(Iio λ) and Iio λ is open
• (v)-(xi) ⟹ (iv): construction of approximating sequence

Derived transitively (by tfae_finish):

• (ix) ⟹ (v) or (vi): via (ix) → (x) → (vii) → (vi) → (v)
• (x) ⟹ (v)-(ix): via (x) → (vii) → (vi) → (v) → (viii)/(ix)

(i) ⟺ (ii): By definition of UnsignedMeasurable

(ii) ⟹ (iii): Pointwise everywhere implies pointwise a.e.

(iv) ⟹ (ii): Monotone sequences in [0,∞] converge to their supremum

(iii) ⟹ (v): Via limsup representation

(v) ⟹ (vi): {f ≥ λ} = ⋂_{n≥1} {f > λ - 1/n}

(vi) ⟹ (v): {f > λ} = ⋃_{q ∈ ℚ, q > λ} {f ≥ q}

(v) ⟹ (viii): {f ≤ t} = {f > t}ᶜ

(vi) ⟹ (vii): {f < t} = {f ≥ t}ᶜ

(vii) ⟹ (vi): {f ≥ t} = {f < t}ᶜ

(viii) ⟹ (v): {f > t} = {f ≤ t}ᶜ

(v)-(viii) ⟹ (ix): Intervals are intersections of half-intervals

(ix) ⟹ (x): Open sets are countable unions of intervals

(x) ⟺ (xi): Complementation

(x) ⟹ (vii): {f < λ} = f⁻¹'(Iio λ) and Iio λ is open

(v)-(xi) ⟹ (iv): Construction of approximating sequence

theorem UnsignedMeasurable.TFAE {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : Unsigned f) : [UnsignedMeasurable f, ∃ (g : ℕ → EuclideanSpace' d → EReal), (∀ (n : ℕ), UnsignedSimpleFunction (g n)) ∧ ∀ (x : EuclideanSpace' d), Filter.Tendsto (fun (n : ℕ) => g n x) Filter.atTop (nhds (f x)), ∃ (g : ℕ → EuclideanSpace' d → EReal), (∀ (n : ℕ), UnsignedSimpleFunction (g n)) ∧ PointwiseAeConvergesTo g f, ∃ (g : ℕ → EuclideanSpace' d → EReal), (∀ (n : ℕ), UnsignedSimpleFunction (g n) ∧ EReal.BoundedFunction (g n) ∧ FiniteMeasureSupport (g n)) ∧ (∀ (x : EuclideanSpace' d), Monotone fun (n : ℕ) => g n x) ∧ ∀ (x : EuclideanSpace' d), f x = ⨆ (n : ℕ), g n x, ∀ (t : EReal), LebesgueMeasurable {x : EuclideanSpace' d | f x > t}, ∀ (t : EReal), LebesgueMeasurable {x : EuclideanSpace' d | f x ≥ t}, ∀ (t : EReal), LebesgueMeasurable {x : EuclideanSpace' d | f x < t}, ∀ (t : EReal), LebesgueMeasurable {x : EuclideanSpace' d | f x ≤ t}, ∀ (I : BoundedInterval), LebesgueMeasurable (f ⁻¹' (Real.toEReal '' ↑I)), ∀ (U : Set EReal), IsOpen U → LebesgueMeasurable (f ⁻¹' U), ∀ (K : Set EReal), IsClosed K → LebesgueMeasurable (f ⁻¹' K)].TFAE

Lemma 1.3.9 (Equivalent notions of measurability). Some slight changes to the statement have been made to make the claims cleaner to state

theorem Continuous.UnsignedMeasurable {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : Continuous f) (hnonneg : Unsigned f) : _root_.UnsignedMeasurable f

Exercise 1.3.3(i)

theorem UnsignedSimpleFunction.unsignedMeasurable {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedSimpleFunction f) : UnsignedMeasurable f

Exercise 1.3.3(ii)

theorem UnsignedMeasurable.sup {d : ℕ} {f : ℕ → EuclideanSpace' d → EReal} (hf : ∀ (n : ℕ), UnsignedMeasurable (f n)) : UnsignedMeasurable fun (x : EuclideanSpace' d) => ⨆ (n : ℕ), f n x

Exercise 1.3.3(iii)

theorem UnsignedMeasurable.inf {d : ℕ} {f : ℕ → EuclideanSpace' d → EReal} (hf : ∀ (n : ℕ), UnsignedMeasurable (f n)) : UnsignedMeasurable fun (x : EuclideanSpace' d) => ⨅ (n : ℕ), f n x

Exercise 1.3.3(iii)

theorem UnsignedMeasurable.limsup {d : ℕ} {f : ℕ → EuclideanSpace' d → EReal} (hf : ∀ (n : ℕ), UnsignedMeasurable (f n)) : UnsignedMeasurable fun (x : EuclideanSpace' d) => Filter.limsup (fun (n : ℕ) => f n x) Filter.atTop

Exercise 1.3.3(iii)

theorem UnsignedMeasurable.liminf {d : ℕ} {f : ℕ → EuclideanSpace' d → EReal} (hf : ∀ (n : ℕ), UnsignedMeasurable (f n)) : UnsignedMeasurable fun (x : EuclideanSpace' d) => Filter.liminf (fun (n : ℕ) => f n x) Filter.atTop

Exercise 1.3.3(iii)

theorem UnsignedMeasurable.aeEqual {d : ℕ} {f g : EuclideanSpace' d → EReal} (hf : UnsignedMeasurable f) (heq : AlmostEverywhereEqual f g) : UnsignedMeasurable g

Exercise 1.3.3(iv)

theorem UnsignedMeasurable.aeLimit {d : ℕ} {f : EuclideanSpace' d → EReal} (g : ℕ → EuclideanSpace' d → EReal) (hf : ∀ (n : ℕ), UnsignedMeasurable (g n)) (heq : PointwiseAeConvergesTo g f) : UnsignedMeasurable f

Exercise 1.3.3(v)

theorem UnsignedMeasurable.comp_cts {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedMeasurable f) {φ : EReal → EReal} (hφ : Continuous φ) : UnsignedMeasurable (φ ∘ f)

Exercise 1.3.3(vi)

theorem UnsignedMeasurable.add {d : ℕ} {f g : EuclideanSpace' d → EReal} (hf : UnsignedMeasurable f) (hg : UnsignedMeasurable g) : UnsignedMeasurable (f + g)

Exercise 1.3.3(vii)

def UniformConvergesTo {X : Type u_1} (f : ℕ → X → EReal) (g : X → EReal) : Prop

Equations

• UniformConvergesTo f g = ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∀ (x : X), f n x > g x - ↑↑ε ∧ f n x < g x + ↑↑ε

theorem UnsignedMeasurable.bounded_iff {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : Unsigned f) : UnsignedMeasurable f ∧ EReal.BoundedFunction f ↔ ∃ (g : ℕ → EuclideanSpace' d → EReal), (∀ (n : ℕ), UnsignedSimpleFunction (g n) ∧ EReal.BoundedFunction (g n)) ∧ UniformConvergesTo g f

Exercise 1.3.4

theorem UnsignedSimpleFunction.iff {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : Unsigned f) : UnsignedSimpleFunction f ↔ UnsignedMeasurable f ∧ Finite ↑(f '' Set.univ)

Exercise 1.3.5

theorem UnsignedMeasurable.measurable_graph {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedMeasurable f) : LebesgueMeasurable {p : EuclideanSpace' (d + 1) | ∃ (x : EuclideanSpace' d) (t : ℝ), (EuclideanSpace'.prod_equiv d 1) p = (x, Real.equiv_EuclideanSpace' t) ∧ 0 ≤ t ∧ ↑t ≤ f x}

Exercise 1.3.6

Remark 1.3.10: Measurable functions can have non-measurable preimages

We construct an example showing that even for a measurable function f: ℝ^d → [0, +∞], the inverse image f⁻¹(E) of a Lebesgue measurable set E need not be Lebesgue measurable.

Strategy (from the textbook):

1. The Cantor set C := {∑ aⱼ 3^{-j} : aⱼ ∈ {0,2}} has measure zero
2. Define f: [0,1] → C by mapping binary digits to ternary: f(∑ bⱼ 2^{-j}) = ∑ 2bⱼ 3^{-j}
3. f is bijective from A (non-terminating binary decimals) onto C, and f is measurable
4. Take non-measurable F ⊆ A (from Vitali construction)
5. E := f(F) ⊆ C is measurable (subset of null set), but f⁻¹(E) = F is non-measurable

Implementation note: Our formalization differs slightly from the textbook:

• Textbook: f(x) = 0 for dyadic rationals (terminating binary decimals)
• Our version: f is defined uniformly for all x ∈ [0,1] using floor-based binary digits

The textbook's f is NOT monotone on [0,1] (e.g., f(0.4) > 0 but f(0.5) = 0). Our f IS monotone on all of [0,1], which simplifies the measurability proof: sublevel sets are intervals, hence measurable by Lemma 1.3.9(viii).

Both versions work for the theorem because:

• Both are injective on A (non-dyadic numbers have unique binary expansions)
• Both map [0,1] into CantorSet ∪ {0}
• Both give measurable f with f⁻¹(E) = F non-measurable

def DyadicRationals : Set ℝ

Dyadic rationals: numbers of the form k/2^n where k ≤ 2^n. These are exactly the real numbers with terminating binary expansions.

Equations

• DyadicRationals = {x : ℝ | ∃ (k : ℕ) (n : ℕ), x = ↑k / 2 ^ n ∧ k ≤ 2 ^ n}

theorem DyadicRationals.countable : DyadicRationals.Countable

Dyadic rationals are countable.

noncomputable def binaryDigit (x : ℝ) (j : ℕ) : ℕ

Binary digit extraction: bⱼ(x) = ⌊2^j · x⌋ mod 2. For x ∈ [0,1), this extracts the j-th binary digit. Special case: x = 1 has all digits = 1 (1 = 0.111...₂). For x ∉ [0,1], all digits are 0.

Equations

• binaryDigit x j = if x ∈ Set.Ico 0 1 then ⌊2 ^ j * x⌋₊ % 2 else if x = 1 then 1 else 0

theorem binaryDigit_le_one (x : ℝ) (j : ℕ) : binaryDigit x j ≤ 1

Binary digits are in {0, 1}.

theorem binaryDigit_zero (j : ℕ) : binaryDigit 0 j = 0

Binary digits of 0 are all 0.

theorem binaryDigit_one (j : ℕ) : binaryDigit 1 j = 1

Binary digits of 1 are all 1.

theorem tsum_two_thirds_geometric : ∑' (j : ℕ), 2 * (1 / 3) ^ (j + 1) = 1

The full sum ∑_{j≥0} 2·(1/3)^{j+1} = 1.

theorem tsum_tail_bound (k : ℕ) : ∑' (j : ℕ), 2 * (1 / 3) ^ (k + j + 1) = (1 / 3) ^ k

The tail sum bound: ∑_{j≥k} 2·(1/3)^{j+1} = (1/3)^k.

theorem floor_two_mul_odd_ge {z : ℝ} (hz : 0 ≤ z) (hodd : ⌊2 * z⌋₊ % 2 = 1) : ⌊2 * z⌋₊ ≥ 2 * ⌊z⌋₊ + 1

Helper: if ⌊2z⌋₊ % 2 = 1 then ⌊2z⌋₊ ≥ 2⌊z⌋₊ + 1

theorem floor_two_mul_even_le {z : ℝ} (hz : 0 ≤ z) (heven : ⌊2 * z⌋₊ % 2 = 0) : ⌊2 * z⌋₊ ≤ 2 * ⌊z⌋₊

Helper: if ⌊2z⌋₊ % 2 = 0 then ⌊2z⌋₊ ≤ 2⌊z⌋₊

theorem floor_two_mul_eq_of_mod_eq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (h_floor : ⌊x⌋₊ = ⌊y⌋₊) (h_mod : ⌊2 * x⌋₊ % 2 = ⌊2 * y⌋₊ % 2) : ⌊2 * x⌋₊ = ⌊2 * y⌋₊

Helper: equal mod 2 and equal ⌊z⌋ implies equal ⌊2z⌋

structure Remark_1_3_10.BinaryToTernaryProperties (g : ℝ → ℝ) : Prop

The properties required of the binary-to-ternary function for this construction. The function maps [0,1] into the Cantor set C by converting binary digits to ternary.

Note: Unlike the textbook (which sets g(x) = 0 for dyadic rationals), our g is defined uniformly for all x ∈ [0,1]. This makes g monotone on ALL of [0,1], not just on A.

• nonneg (x : ℝ) : 0 ≤ g x
• bounded (x : ℝ) : g x ≤ 1
• zero_outside (x : ℝ) : x ∉ Set.Icc 0 1 → g x = 0
• zero_at_zero : g 0 = 0
• zero_set_countable : (Set.Icc 0 1 ∩ {x : ℝ | g x = 0}).Countable
• monotone_on : MonotoneOn g (Set.Icc 0 1)
• image_in_cantor : g '' Set.Icc 0 1 ⊆ CantorSet ∪ {0}
• injective_on_nonterminating : ∃ A ⊆ Set.Icc 0 1, (Set.Icc 0 1 \ A).Countable ∧ Set.InjOn g A ∧ A ∩ DyadicRationals = ∅

noncomputable def Remark_1_3_10.binaryToTernaryFn (x : ℝ) : ℝ

The binary-to-ternary function: g(x) = ∑_{j≥1} 2·bⱼ(x)·3^{-j} for x ∈ [0,1], else 0.

Equations

• Remark_1_3_10.binaryToTernaryFn x = if x ∈ Set.Icc 0 1 then ∑' (j : ℕ), 2 * ↑(binaryDigit x (j + 1)) * (1 / 3) ^ (j + 1) else 0

theorem Remark_1_3_10.binaryToTernary_summable (x : ℝ) : Summable fun (j : ℕ) => 2 * ↑(binaryDigit x (j + 1)) * (1 / 3) ^ (j + 1)

The series ∑ 2·bⱼ(x)·3^{-j} is summable for any x.

Helper lemmas for monotonicity proof

theorem Remark_1_3_10.binaryDigit_exists_one_of_pos {x : ℝ} (hx_pos : 0 < x) (hx_lt : x < 1) : ∃ (j : ℕ), binaryDigit x (j + 1) = 1

For x ∈ (0, 1), there exists a position where the binary digit is 1.

theorem Remark_1_3_10.binaryDigit_partial_sum_le {x : ℝ} (hx : x ∈ Set.Ico 0 1) (n : ℕ) : ↑⌊2 ^ n * x⌋₊ / 2 ^ n ≤ x

The partial sum bounds x from below: Sₙ(x) ≤ x

theorem Remark_1_3_10.binaryDigit_partial_sum_lt (x : ℝ) (n : ℕ) : x < ↑⌊2 ^ n * x⌋₊ / 2 ^ n + 1 / 2 ^ n

The partial sum bounds x from above: x < Sₙ(x) + 2^{-n}

theorem Remark_1_3_10.binaryDigit_one_implies_lower_bound {x : ℝ} (hx : x ∈ Set.Ico 0 1) (k : ℕ) (hbk : binaryDigit x (k + 1) = 1) : ↑⌊2 ^ k * x⌋₊ / 2 ^ k + 1 / 2 ^ (k + 1) ≤ x

Key lemma: if bₖ(x) = 1, then x ≥ ⌊2^k * x⌋₊ / 2^k + 2^{-(k+1)}

theorem Remark_1_3_10.binaryDigit_zero_implies_upper_bound {y : ℝ} (hy : y ∈ Set.Ico 0 1) (k : ℕ) (hbk : binaryDigit y (k + 1) = 0) : y < ↑⌊2 ^ k * y⌋₊ / 2 ^ k + 1 / 2 ^ (k + 1)

Key lemma: if bₖ(y) = 0, then y < ⌊2^k * y⌋₊ / 2^k + 2^{-(k+1)}

theorem Remark_1_3_10.floor_eq_of_binaryDigit_eq {n : ℕ} {x y : ℝ} (hx : x ∈ Set.Ico 0 1) (hy : y ∈ Set.Ico 0 1) (heq : ∀ j < n, binaryDigit x (j + 1) = binaryDigit y (j + 1)) : ⌊2 ^ n * x⌋₊ = ⌊2 ^ n * y⌋₊

Helper: floors of x, y in [0,1) are equal up to level n if their binary digits agree up to level n-1.

theorem Remark_1_3_10.binaryDigit_first_diff {x y : ℝ} (hx : x ∈ Set.Ico 0 1) (hy : y ∈ Set.Ico 0 1) (hxy : x < y) : ∃ (k : ℕ), binaryDigit x (k + 1) < binaryDigit y (k + 1) ∧ ∀ j < k, binaryDigit x (j + 1) = binaryDigit y (j + 1)

For x, y ∈ [0,1) with x < y, there exists a first position k where bₖ(x) < bₖ(y).

theorem Remark_1_3_10.binaryToTernary_lt_of_digit_lt {x y : ℝ} (hx : x ∈ Set.Icc 0 1) (hy : y ∈ Set.Icc 0 1) (k : ℕ) (hk_lt : binaryDigit x (k + 1) < binaryDigit y (k + 1)) (hk_eq : ∀ j < k, binaryDigit x (j + 1) = binaryDigit y (j + 1)) : binaryToTernaryFn x < binaryToTernaryFn y

Monotonicity: if digits agree up to k and bₖ(x) < bₖ(y), then g(x) < g(y).

Helper lemmas for injectivity proof

theorem Remark_1_3_10.ternary_02_expansion_unique {d e : ℕ → ℕ} (hd : ∀ (j : ℕ), d j ∈ {0, 2}) (he : ∀ (j : ℕ), e j ∈ {0, 2}) (hsum_d : Summable fun (j : ℕ) => ↑(d j) * (1 / 3) ^ (j + 1)) (hsum_e : Summable fun (j : ℕ) => ↑(e j) * (1 / 3) ^ (j + 1)) (heq : ∑' (j : ℕ), ↑(d j) * (1 / 3) ^ (j + 1) = ∑' (j : ℕ), ↑(e j) * (1 / 3) ^ (j + 1)) (j : ℕ) : d j = e j

Ternary {0,2} expansions are unique.

Helper lemmas for binary expansion sums

theorem Remark_1_3_10.non_dyadic_eq_binary_sum {x : ℝ} (hx : x ∈ Set.Ico 0 1) (_hnd : x ∉ DyadicRationals) : x = ∑' (j : ℕ), ↑(binaryDigit x (j + 1)) * (1 / 2) ^ (j + 1)

For non-dyadic x ∈ [0,1), x equals its binary expansion sum.

theorem Remark_1_3_10.eq_of_binaryDigit_eq_of_non_dyadic {x₁ x₂ : ℝ} (hx₁ : x₁ ∈ Set.Ico 0 1) (hx₂ : x₂ ∈ Set.Ico 0 1) (hnd₁ : x₁ ∉ DyadicRationals) (hnd₂ : x₂ ∉ DyadicRationals) (heq : ∀ (j : ℕ), binaryDigit x₁ j = binaryDigit x₂ j) : x₁ = x₂

Non-dyadic x ∈ [0,1) with equal binary digits are equal.

Helper lemmas for image_in_cantor

theorem Remark_1_3_10.mem_CantorSet_of_ternary_02 {y : ℝ} (d : ℕ → ℕ) (hd : ∀ (j : ℕ), d j ∈ {0, 2}) (hsum : Summable fun (j : ℕ) => ↑(d j) * (1 / 3) ^ (j + 1)) (hy : y = ∑' (j : ℕ), ↑(d j) * (1 / 3) ^ (j + 1)) : y ∈ CantorSet ∨ y = 0

Points with {0,2} ternary digits are in the Cantor set.

theorem Remark_1_3_10.binaryToTernary_exists : ∃ (g : ℝ → ℝ), BinaryToTernaryProperties g

Existence of a binary-to-ternary function: g(x) = ∑ 2bⱼ 3^{-j}.

noncomputable def Remark_1_3_10.binaryToTernary : ℝ → ℝ

Binary-to-ternary function: g(x) = ∑ 2·bⱼ(x)·3^{-j}, monotone on [0,1], g([0,1]) ⊆ C ∪ {0}.

Equations

• Remark_1_3_10.binaryToTernary = Classical.choose Remark_1_3_10.binaryToTernary_exists

theorem Remark_1_3_10.binaryToTernary_props : BinaryToTernaryProperties binaryToTernary

theorem Remark_1_3_10.binaryToTernary_eq_zero_iff {x : ℝ} (hx : x ∈ Set.Icc 0 1) : binaryToTernary x = 0 ↔ x = 0

binaryToTernary x = 0 iff x = 0 for x ∈ [0,1].

noncomputable def Remark_1_3_10.f_lifted : EuclideanSpace' 1 → EReal

binaryToTernary lifted to EuclideanSpace' 1 → EReal (called f in informal proof).

Equations

• Remark_1_3_10.f_lifted x = ↑(max 0 (Remark_1_3_10.binaryToTernary (EuclideanSpace'.equiv_Real x)))

theorem Remark_1_3_10.f_lifted_unsigned : Unsigned f_lifted

theorem Remark_1_3_10.f_lifted_le_one (x : EuclideanSpace' 1) : f_lifted x ≤ 1

theorem Remark_1_3_10.f_lifted_zero_outside (x : EuclideanSpace' 1) (hx : EuclideanSpace'.equiv_Real x ∉ Set.Icc 0 1) : f_lifted x = 0

theorem Remark_1_3_10.f_lifted_zero_at_zero (x : EuclideanSpace' 1) (hx : EuclideanSpace'.equiv_Real x = 0) : f_lifted x = 0

theorem Remark_1_3_10.f_zero_set_in_interval_countable : (Set.Icc 0 1 ∩ {x : ℝ | binaryToTernary x = 0}).Countable

theorem Remark_1_3_10.f_lifted_zero_set_measurable : LebesgueMeasurable {x : EuclideanSpace' 1 | f_lifted x = 0}

theorem Remark_1_3_10.sublevel_set_measurable (t : EReal) (ht_pos : 0 < t) (ht_lt_one : t < 1) : LebesgueMeasurable {x : EuclideanSpace' 1 | f_lifted x ≤ t}

Sublevel sets of f_lifted are measurable (key lemma for f_lifted_measurable).

theorem Remark_1_3_10.f_lifted_measurable : UnsignedMeasurable f_lifted

theorem Remark_1_3_10.exists_nonmeasurable_with_cantor_image : ∃ (F : Set ℝ) (A : Set ℝ), F ⊆ Set.Icc 0 1 ∧ ¬LebesgueMeasurable (⇑Real.equiv_EuclideanSpace' '' F) ∧ binaryToTernary '' F ⊆ CantorSet ∧ F ⊆ A ∧ A ⊆ Set.Icc 0 1 ∧ (Set.Icc 0 1 \ A).Countable ∧ Set.InjOn binaryToTernary A

Non-measurable F ⊆ [0,1] with binaryToTernary(F) ⊆ Cantor set (Vitali construction).

def ComplexMeasurable {d : ℕ} (f : EuclideanSpace' d → ℂ) : Prop

Definition 1.3.11 (Complex measurability)

Equations

• ComplexMeasurable f = ∃ (g : ℕ → EuclideanSpace' d → ℂ), (∀ (n : ℕ), ComplexSimpleFunction (g n)) ∧ PointwiseConvergesTo g f

def RealMeasurable {d : ℕ} (f : EuclideanSpace' d → ℝ) : Prop

Equations

• RealMeasurable f = ∃ (g : ℕ → EuclideanSpace' d → ℝ), (∀ (n : ℕ), RealSimpleFunction (g n)) ∧ PointwiseConvergesTo g f

theorem RealMeasurable.iff {d : ℕ} {f : EuclideanSpace' d → ℝ} : RealMeasurable f ↔ ComplexMeasurable (Real.complex_fun f)

theorem ComplexMeasurable.iff {d : ℕ} {f : EuclideanSpace' d → ℂ} : ComplexMeasurable f ↔ RealMeasurable (Complex.re_fun f) ∧ RealMeasurable (Complex.im_fun f)

theorem RealMeasurable.TFAE {d : ℕ} {f : EuclideanSpace' d → ℝ} : [RealMeasurable f, ∃ (g : ℕ → EuclideanSpace' d → ℝ), (∀ (n : ℕ), RealSimpleFunction (g n)) ∧ PointwiseAeConvergesTo g f, UnsignedMeasurable (EReal.pos_fun f) ∧ UnsignedMeasurable (EReal.neg_fun f), ∀ (U : Set ℝ), IsOpen U → MeasurableSet (f ⁻¹' U), ∀ (K : Set ℝ), IsClosed K → MeasurableSet (f ⁻¹' K)].TFAE

Exercise 1.3.7

theorem ComplexMeasurable.TFAE {d : ℕ} {f : EuclideanSpace' d → ℂ} : [ComplexMeasurable f, ∃ (g : ℕ → EuclideanSpace' d → ℂ), (∀ (n : ℕ), ComplexSimpleFunction (g n)) ∧ PointwiseAeConvergesTo g f, RealMeasurable (Complex.re_fun f) ∧ RealMeasurable (Complex.im_fun f), UnsignedMeasurable (EReal.pos_fun (Complex.re_fun f)) ∧ UnsignedMeasurable (EReal.neg_fun (Complex.im_fun f)) ∧ UnsignedMeasurable (EReal.pos_fun (Complex.im_fun f)) ∧ UnsignedMeasurable (EReal.neg_fun (Complex.re_fun f)), ∀ (U : Set ℂ), IsOpen U → MeasurableSet (f ⁻¹' U), ∀ (K : Set ℂ), IsClosed K → MeasurableSet (f ⁻¹' K)].TFAE

theorem Continuous.RealMeasurable {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : Continuous f) : _root_.RealMeasurable f

Exercise 1.3.8(i)

theorem Continuous.ComplexMeasurable {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : Continuous f) : _root_.ComplexMeasurable f

theorem UnsignedSimpleFunction.iff' {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : Unsigned f) : UnsignedSimpleFunction f ↔ UnsignedMeasurable f ∧ Finite ↑(f '' Set.univ)

Exercise 1.3.8(ii)

theorem RealMeasurable.aeEqual {d : ℕ} {f g : EuclideanSpace' d → ℝ} (hf : RealMeasurable f) (heq : AlmostEverywhereEqual f g) : RealMeasurable g

Exercise 1.3.8(iii)

theorem ComplexMeasurable.aeEqual {d : ℕ} {f g : EuclideanSpace' d → ℂ} (hf : ComplexMeasurable f) (heq : AlmostEverywhereEqual f g) : ComplexMeasurable g

theorem RealMeasurable.aeLimit {d : ℕ} {f : EuclideanSpace' d → ℝ} (g : ℕ → EuclideanSpace' d → ℝ) (hf : ∀ (n : ℕ), RealMeasurable (g n)) (heq : PointwiseAeConvergesTo g f) : RealMeasurable f

Exercise 1.3.8(iv)

theorem ComplexMeasurable.aeLimit {d : ℕ} {f : EuclideanSpace' d → ℂ} (g : ℕ → EuclideanSpace' d → ℂ) (hf : ∀ (n : ℕ), ComplexMeasurable (g n)) (heq : PointwiseAeConvergesTo g f) : ComplexMeasurable f

theorem RealMeasurable.comp_cts {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealMeasurable f) {φ : ℝ → ℝ} (hφ : Continuous φ) : RealMeasurable (φ ∘ f)

Exercise 1.3.8(v)

theorem ComplexMeasurable.comp_cts {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexMeasurable f) {φ : ℂ → ℂ} (hφ : Continuous φ) : ComplexMeasurable (φ ∘ f)

theorem RealMeasurable.add {d : ℕ} {f g : EuclideanSpace' d → ℝ} (hf : RealMeasurable f) (hg : RealMeasurable g) : RealMeasurable (f + g)

Exercise 1.3.8(vi)

theorem ComplexMeasurable.add {d : ℕ} {f g : EuclideanSpace' d → ℂ} (hf : ComplexMeasurable f) (hg : ComplexMeasurable g) : ComplexMeasurable (f + g)

theorem RealMeasurable.sub {d : ℕ} {f g : EuclideanSpace' d → ℝ} (hf : RealMeasurable f) (hg : RealMeasurable g) : RealMeasurable (f - g)

Exercise 1.3.8(vi)

theorem ComplexMeasurable.sub {d : ℕ} {f g : EuclideanSpace' d → ℂ} (hf : ComplexMeasurable f) (hg : ComplexMeasurable g) : ComplexMeasurable (f - g)

theorem RealMeasurable.mul {d : ℕ} {f g : EuclideanSpace' d → ℝ} (hf : RealMeasurable f) (hg : RealMeasurable g) : RealMeasurable (f * g)

Exercise 1.3.8(vi)

theorem ComplexMeasurable.mul {d : ℕ} {f g : EuclideanSpace' d → ℂ} (hf : ComplexMeasurable f) (hg : ComplexMeasurable g) : ComplexMeasurable (f * g)

theorem RealMeasurable.riemann_integrable {f : ℝ → ℝ} {I : BoundedInterval} (hf : RiemannIntegrableOn f I) : RealMeasurable ((fun (x : ℝ) => if x ∈ ↑I then f x else 0) ∘ ⇑EuclideanSpace'.equiv_Real)

Exercise 1.3.9