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

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), MeasurableSet {x : EuclideanSpace' d | f x > t}, ∀ (t : EReal), MeasurableSet {x : EuclideanSpace' d | f x ≥ t}, ∀ (t : EReal), MeasurableSet {x : EuclideanSpace' d | f x < t}, ∀ (t : EReal), MeasurableSet {x : EuclideanSpace' d | f x ≤ t}, ∀ (I : BoundedInterval), MeasurableSet (f ⁻¹' (Real.toEReal '' ↑I)), ∀ (U : Set EReal), IsOpen U → MeasurableSet (f ⁻¹' U), ∀ (K : Set EReal), IsClosed K → MeasurableSet (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