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

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