Introduction to Measure Theory, Section 1.3.1: Integration of simple functions

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

def EReal.abs_fun {X : Type u_1} {Y : Type u_2} [RCLike Y] (f : X → Y) : X → EReal

Equations

• EReal.abs_fun f x = ↑‖f x‖

def Complex.re_fun {X : Type u_1} (f : X → ℂ) : X → ℝ

Equations

• Complex.re_fun f x = (f x).re

def Complex.im_fun {X : Type u_1} (f : X → ℂ) : X → ℝ

Equations

• Complex.im_fun f x = (f x).im

def Complex.conj_fun {X : Type u_1} (f : X → ℂ) : X → ℂ

Equations

• Complex.conj_fun f x = (starRingEnd ℂ) (f x)

def EReal.pos_fun {X : Type u_1} (f : X → ℝ) : X → EReal

Equations

• EReal.pos_fun f x = ↑(max (f x) 0)

def EReal.neg_fun {X : Type u_1} (f : X → ℝ) : X → EReal

Equations

• EReal.neg_fun f x = ↑(max (-f x) 0)

def Real.complex_fun {X : Type u_1} (f : X → ℝ) : X → ℂ

Equations

• Real.complex_fun f x = ↑(f x)

def Real.EReal_fun {X : Type u_1} (f : X → ℝ) : X → EReal

Equations

• Real.EReal_fun f x = ↑(f x)

noncomputable def EReal.indicator {X : Type u_1} (A : Set X) : X → EReal

Equations

• EReal.indicator A = Real.EReal_fun A.indicator'

noncomputable def Complex.indicator {X : Type u_1} (A : Set X) : X → ℂ

Equations

• Complex.indicator A = Real.complex_fun A.indicator'

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

Definition 1.3.2

Equations

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

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

Equations

• RealSimpleFunction f = ∃ (k : ℕ) (c : Fin k → ℝ) (E : Fin k → Set (EuclideanSpace' d)), (∀ (i : Fin k), LebesgueMeasurable (E i)) ∧ f = ∑ i : Fin k, c i • (E i).indicator'

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

Equations

• ComplexSimpleFunction f = ∃ (k : ℕ) (c : Fin k → ℝ) (E : Fin k → Set (EuclideanSpace' d)), (∀ (i : Fin k), LebesgueMeasurable (E i)) ∧ f = ∑ i : Fin k, c i • Complex.indicator (E i)

@[reducible, inline]

abbrev RealSimpleFunction.toComplex {d : ℕ} (f : EuclideanSpace' d → ℝ) (df : RealSimpleFunction f) : ComplexSimpleFunction (Real.complex_fun f)

Equations

• ⋯ = ⋯

instance RealSimpleFunction.coe_complex {d : ℕ} (f : EuclideanSpace' d → ℝ) : Coe (RealSimpleFunction f) (ComplexSimpleFunction (Real.complex_fun f))

Equations

• RealSimpleFunction.coe_complex f = { coe := ⋯ }

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

theorem UnsignedSimpleFunction.smul {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedSimpleFunction f) {a : EReal} (ha : a ≥ 0) : UnsignedSimpleFunction (a • f)

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

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

theorem RealSimpleFunction.smul {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealSimpleFunction f) (a : ℝ) : RealSimpleFunction (a • f)

theorem ComplexSimpleFunction.smul {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexSimpleFunction f) (a : ℂ) : ComplexSimpleFunction (a • f)

theorem ComplexSimpleFunction.conj {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexSimpleFunction f) : ComplexSimpleFunction (Complex.conj_fun f)

noncomputable def UnsignedSimpleFunction.integ {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedSimpleFunction f) : EReal

Equations

• hf.integ = ∑ i : Fin (Exists.choose hf), ⋯.choose i * Lebesgue_measure (⋯.choose i)

theorem UnsignedSimpleFunction.integral_eq {d : ℕ} {f f✝ : EuclideanSpace' d → EReal} (hf : UnsignedSimpleFunction f✝) {k : ℕ} {c : Fin k → EReal} {E : Fin k → Set (EuclideanSpace' d)} (hmes : ∀ (i : Fin k), LebesgueMeasurable (E i)) (hnonneg : ∀ (i : Fin k), c i ≥ 0) (heq : f✝ = ∑ i : Fin k, c i • EReal.indicator (E i)) : hf.integ = ∑ i : Fin (Exists.choose hf), ⋯.choose i * Lebesgue_measure (⋯.choose i)

Lemma 1.3.4 (Well-definedness of simple integral)

def AlmostAlways {d : ℕ} (P : EuclideanSpace' d → Prop) : Prop

Definition 1.3.5

Equations

• AlmostAlways P = IsNull {x : EuclideanSpace' d | ¬P x}

def AlmostEverywhereEqual {d : ℕ} {X : Type u_1} (f g : EuclideanSpace' d → X) : Prop

Definition 1.3.5

Equations

• AlmostEverywhereEqual f g = AlmostAlways fun (x : EuclideanSpace' d) => f x = g x

def Support {X : Type u_1} {Y : Type u_2} [Zero Y] (f : X → Y) : Set X

Definition 1.3.5

Equations

• Support f = {x : X | f x ≠ 0}

theorem UnsignedSimpleFunction.support_measurable {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedSimpleFunction f) : LebesgueMeasurable (Support f)

theorem AlmostAlways.ofAlways {d : ℕ} {P : EuclideanSpace' d → Prop} (h : ∀ (x : EuclideanSpace' d), P x) : AlmostAlways P

theorem AlmostAlways.mp {d : ℕ} {P Q : EuclideanSpace' d → Prop} (hP : AlmostAlways P) (himp : ∀ (x : EuclideanSpace' d), P x → Q x) : AlmostAlways Q

theorem AlmostAlways.countable {d : ℕ} {I : Type u_1} [Countable I] {P : I → EuclideanSpace' d → Prop} (hP : ∀ (i : I), AlmostAlways (P i)) : AlmostAlways fun (x : EuclideanSpace' d) => ∀ (i : I), P i x

theorem UnsignedSimpleFunction.integral_add {d : ℕ} {f g : EuclideanSpace' d → EReal} (hf : UnsignedSimpleFunction f) (hg : UnsignedSimpleFunction g) : ⋯.integ = hf.integ + hg.integ

Exercise 1.3.1 (i) (Unsigned linearity)

theorem UnsignedSimpleFunction.integral_smul {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedSimpleFunction f) {c : EReal} (hc : c ≥ 0) : ⋯.integ = c * hf.integ

Exercise 1.3.1 (i) (Unsigned linearity)

theorem UnsignedSimpleFunction.integral_finite_iff {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedSimpleFunction f) : hf.integ < ⊤ ↔ (AlmostAlways fun (x : EuclideanSpace' d) => f x < ⊤) ∧ Lebesgue_measure (Support f) < ⊤

Exercise 1.3.1 (ii) (Finiteness)

theorem UnsignedSimpleFunction.integral_eq_zero_iff {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedSimpleFunction f) : hf.integ = 0 ↔ AlmostAlways fun (x : EuclideanSpace' d) => f x = 0

Exercise 1.3.1 (iii) (Vanishing)

theorem UnsignedSimpleFunction.integral_eq_integral_of_aeEqual {d : ℕ} {f g : EuclideanSpace' d → EReal} (hf : UnsignedSimpleFunction f) (hg : UnsignedSimpleFunction g) (hae : AlmostEverywhereEqual f g) : hf.integ = hg.integ

Exercise 1.3.1 (iv) (Equivalence)

theorem UnsignedSimpleFunction.integral_le_integral_of_aeLe {d : ℕ} {f g : EuclideanSpace' d → EReal} (hf : UnsignedSimpleFunction f) (hg : UnsignedSimpleFunction g) (hae : AlmostAlways fun (x : EuclideanSpace' d) => f x ≤ g x) : hf.integ ≤ hg.integ

Exercise 1.3.1 (v) (Monotonicity)

theorem UnsignedSimpleFunction.indicator {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) : UnsignedSimpleFunction (Real.toEReal ∘ E.indicator')

Exercise 1.3.1(vi) (Compatibility with Lebesgue measure)

theorem UnsignedSimpleFunction.integral_indicator {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) : ⋯.integ = Lebesgue_measure E

Exercise 1.3.1(vi) (Compatibility with Lebesgue measure)

theorem RealSimpleFunction.abs {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealSimpleFunction f) : UnsignedSimpleFunction (EReal.abs_fun f)

theorem ComplexSimpleFunction.abs {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexSimpleFunction f) : UnsignedSimpleFunction (EReal.abs_fun f)

def RealSimpleFunction.AbsolutelyIntegrable {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealSimpleFunction f) : Prop

Definition 1.3.6 (Absolutely convergent simple integral)

Equations

• hf.AbsolutelyIntegrable = (⋯.integ < ⊤)

def ComplexSimpleFunction.AbsolutelyIntegrable {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexSimpleFunction f) : Prop

Definition 1.3.6 (Absolutely convergent simple integral)

Equations

• hf.AbsolutelyIntegrable = (⋯.integ < ⊤)

def RealSimpleFunction.pos {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealSimpleFunction f) : UnsignedSimpleFunction (EReal.pos_fun f)

Equations

• ⋯ = ⋯

def RealSimpleFunction.neg {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealSimpleFunction f) : UnsignedSimpleFunction (EReal.neg_fun f)

Equations

• ⋯ = ⋯

noncomputable def RealSimpleFunction.integ {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealSimpleFunction f) : ℝ

Equations

• hf.integ = ⋯.integ.toReal - ⋯.integ.toReal

def ComplexSimpleFunction.re {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexSimpleFunction f) : RealSimpleFunction (Complex.re_fun f)

Equations

• ⋯ = ⋯

def ComplexSimpleFunction.im {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexSimpleFunction f) : RealSimpleFunction (Complex.im_fun f)

Equations

• ⋯ = ⋯

noncomputable def ComplexSimpleFunction.integ {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexSimpleFunction f) : ℂ

Equations

• hf.integ = ↑⋯.integ + Complex.I * ↑⋯.integ

theorem RealSimpleFunction.absolutelyIntegrable_iff {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealSimpleFunction f) : hf.AbsolutelyIntegrable ↔ Lebesgue_measure (Support f) < ⊤

theorem ComplexSimpleFunction.absolutelyIntegrable_iff {d : ℕ} {f : EuclideanSpace' d → ℂ} (hf : ComplexSimpleFunction f) : hf.AbsolutelyIntegrable ↔ Lebesgue_measure (Support f) < ⊤

theorem RealSimpleFunction.AbsolutelyIntegrable.add {d : ℕ} {f g : EuclideanSpace' d → ℝ} {hf : RealSimpleFunction f} {hg : RealSimpleFunction g} (hf_integ : hf.AbsolutelyIntegrable) (hg_integ : hg.AbsolutelyIntegrable) : ⋯.AbsolutelyIntegrable

theorem ComplexSimpleFunction.AbsolutelyIntegrable.add {d : ℕ} {f g : EuclideanSpace' d → ℂ} {hf : ComplexSimpleFunction f} {hg : ComplexSimpleFunction g} (hf_integ : hf.AbsolutelyIntegrable) (hg_integ : hg.AbsolutelyIntegrable) : ⋯.AbsolutelyIntegrable

theorem RealSimpleFunction.AbsolutelyIntegrable.smul {d : ℕ} {f : EuclideanSpace' d → ℝ} {hf : RealSimpleFunction f} (hf_integ : hf.AbsolutelyIntegrable) (a : ℝ) : ⋯.AbsolutelyIntegrable

theorem ComplexSimpleFunction.AbsolutelyIntegrable.smul {d : ℕ} {f : EuclideanSpace' d → ℂ} {hf : ComplexSimpleFunction f} (hf_integ : hf.AbsolutelyIntegrable) (a : ℂ) : ⋯.AbsolutelyIntegrable

theorem ComplexSimpleFunction.AbsolutelyIntegrable.conj {d : ℕ} {f : EuclideanSpace' d → ℂ} {hf : ComplexSimpleFunction f} (hf_integ : hf.AbsolutelyIntegrable) : ⋯.AbsolutelyIntegrable

theorem RealSimpleFunction.integ_add {d : ℕ} {f g : EuclideanSpace' d → ℝ} {hf : RealSimpleFunction f} {hg : RealSimpleFunction g} (hf_integ : hf.AbsolutelyIntegrable) (hg_integ : hg.AbsolutelyIntegrable) : ⋯.integ = hf.integ + hg.integ

Exercise 1.3.2 (i) (*-linearity)

theorem ComplexSimpleFunction.integ_add {d : ℕ} {f g : EuclideanSpace' d → ℂ} {hf : ComplexSimpleFunction f} {hg : ComplexSimpleFunction g} (hf_integ : hf.AbsolutelyIntegrable) (hg_integ : hg.AbsolutelyIntegrable) : ⋯.integ = hf.integ + hg.integ

theorem RealSimpleFunction.integ_smul {d : ℕ} {f : EuclideanSpace' d → ℝ} {hf : RealSimpleFunction f} (hf_integ : hf.AbsolutelyIntegrable) (a : ℝ) : ⋯.integ = a * hf.integ

Exercise 1.3.2 (i) (*-linearity)

theorem ComplexSimpleFunction.integ_smul {d : ℕ} {f : EuclideanSpace' d → ℂ} {hf : ComplexSimpleFunction f} (hf_integ : hf.AbsolutelyIntegrable) (a : ℂ) : ⋯.integ = a * hf.integ

theorem ComplexSimpleFunction.integral_conj {d : ℕ} {f : EuclideanSpace' d → ℂ} {hf : ComplexSimpleFunction f} (hf_integ : hf.AbsolutelyIntegrable) : ⋯.integ = (starRingEnd ℂ) hf.integ

Exercise 1.3.2 (i) (*-linearity)

theorem RealSimpleFunction.integral_eq_integral_of_aeEqual {d : ℕ} {f g : EuclideanSpace' d → ℝ} {hf : RealSimpleFunction f} {hg : RealSimpleFunction g} (hf_integ : hf.AbsolutelyIntegrable) (hg_integ : hg.AbsolutelyIntegrable) (h_ae : AlmostEverywhereEqual f g) : hf.integ = hg.integ

Exercise 1.3.2 (ii) (equivalence)

theorem ComplexSimpleFunction.integral_eq_integral_of_aeEqual {d : ℕ} {f g : EuclideanSpace' d → ℂ} {hf : ComplexSimpleFunction f} {hg : ComplexSimpleFunction g} (hf_integ : hf.AbsolutelyIntegrable) (hg_integ : hg.AbsolutelyIntegrable) (h_ae : AlmostEverywhereEqual f g) : hf.integ = hg.integ

theorem RealSimpleFunction.indicator {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) : RealSimpleFunction E.indicator'

Exercise 1.3.2(iii) (Compatibility with Lebesgue measure)

theorem ComplexSimpleFunction.indicator {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) : ComplexSimpleFunction (Complex.indicator E)

theorem RealSimpleFunction.integral_indicator {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) (hfin : Lebesgue_measure E < ⊤) : ⋯.integ = (Lebesgue_measure E).toReal

Exercise 1.3.2(iii) (Compatibility with Lebesgue measure)

theorem ComplexSimpleFunction.integral_indicator {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) (hfin : Lebesgue_measure E < ⊤) : ⋯.integ = ↑(Lebesgue_measure E).toReal