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)

Helper lemmas for Lemma 1.3.4

The proof uses a Venn diagram argument: given two representations of the same simple function, we partition R^d into atoms (intersections of all sets and their complements), express each original set as a disjoint union of atoms, and use finite additivity of Lebesgue measure.

def UnsignedSimpleFunction.IntegralWellDef.atomMembership (_k _k' n i : ℕ) : Bool

Given families of sets indexed by Fin k and Fin k', an atom is determined by a choice of "in" or "out" for each set. We encode this as a Fin (2^(k+k')) index.

Equations

• UnsignedSimpleFunction.IntegralWellDef.atomMembership _k _k' n i = decide (n / 2 ^ i % 2 = 1)

theorem UnsignedSimpleFunction.IntegralWellDef.atomMembership_eq_testBit (k k' n i : ℕ) : atomMembership k k' n i = n.testBit i

def UnsignedSimpleFunction.IntegralWellDef.atom {X : Type u_1} {k k' : ℕ} (E : Fin k → Set X) (E' : Fin k' → Set X) (n : Fin (2 ^ (k + k'))) : Set X

The atom indexed by n is the intersection over all i of (E_i if bit i is 1, else E_i^c)

Equations

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

theorem UnsignedSimpleFunction.IntegralWellDef.atom_pairwiseDisjoint {X : Type u_1} {k k' : ℕ} (E : Fin k → Set X) (E' : Fin k' → Set X) : Set.univ.PairwiseDisjoint (atom E E')

Atoms are pairwise disjoint

noncomputable def UnsignedSimpleFunction.IntegralWellDef.atomIndexOf {X : Type u_1} [DecidableEq X] {k k' : ℕ} (E : Fin k → Set X) (E' : Fin k' → Set X) (x : X) : ℕ

Helper: construct atom index from membership pattern. The atom index encodes x's membership in each set as bits.

Equations

• UnsignedSimpleFunction.IntegralWellDef.atomIndexOf E E' x = ∑ j : Fin k with x ∈ E j, 2 ^ ↑j + ∑ j' : Fin k' with x ∈ E' j', 2 ^ (k + ↑j')

theorem UnsignedSimpleFunction.IntegralWellDef.atomIndexOf_lt {X : Type u_1} [DecidableEq X] {k k' : ℕ} (E : Fin k → Set X) (E' : Fin k' → Set X) (x : X) : atomIndexOf E E' x < 2 ^ (k + k')

The atom index is bounded by 2^(k+k')

theorem UnsignedSimpleFunction.IntegralWellDef.atomIndexOf_testBit_E {X : Type u_1} [DecidableEq X] {k k' : ℕ} (E : Fin k → Set X) (E' : Fin k' → Set X) (x : X) (j : Fin k) : (atomIndexOf E E' x).testBit ↑j = true ↔ x ∈ E j

The atom index has bit j set iff x ∈ E j

theorem UnsignedSimpleFunction.IntegralWellDef.atomIndexOf_testBit_E' {X : Type u_1} [DecidableEq X] {k k' : ℕ} (E : Fin k → Set X) (E' : Fin k' → Set X) (x : X) (j : Fin k') : (atomIndexOf E E' x).testBit (k + ↑j) = true ↔ x ∈ E' j

The atom index has bit (k+j) set iff x ∈ E' j

theorem UnsignedSimpleFunction.IntegralWellDef.set_eq_biUnion_atoms {X : Type u_1} {k k' : ℕ} (E : Fin k → Set X) (E' : Fin k' → Set X) (i : Fin k) : E i = ⋃ n ∈ {n : Fin (2 ^ (k + k')) | atomMembership k k' ↑n ↑i = true}, atom E E' n

Original set E_i is the union of atoms where bit i is 1

theorem UnsignedSimpleFunction.IntegralWellDef.set_eq_biUnion_atoms' {X : Type u_1} {k k' : ℕ} (E : Fin k → Set X) (E' : Fin k' → Set X) (i : Fin k') : E' i = ⋃ n ∈ {n : Fin (2 ^ (k + k')) | atomMembership k k' (↑n) (k + ↑i) = true}, atom E E' n

Original set E'_i is the union of atoms where bit (k+i) is 1

theorem UnsignedSimpleFunction.IntegralWellDef.atom_measurable {d k k' : ℕ} {E : Fin k → Set (EuclideanSpace' d)} {E' : Fin k' → Set (EuclideanSpace' d)} (hE : ∀ (i : Fin k), LebesgueMeasurable (E i)) (hE' : ∀ (i : Fin k'), LebesgueMeasurable (E' i)) (n : Fin (2 ^ (k + k'))) : LebesgueMeasurable (atom E E' n)

Atoms are measurable if the original sets are

theorem UnsignedSimpleFunction.IntegralWellDef.indicator_mul_mem {d : ℕ} (E : Set (EuclideanSpace' d)) (c : EReal) (x : EuclideanSpace' d) (h : x ∈ E) : c * EReal.indicator E x = c

Indicator function evaluates to c if x ∈ E

theorem UnsignedSimpleFunction.IntegralWellDef.indicator_mul_not_mem {d : ℕ} (E : Set (EuclideanSpace' d)) (c : EReal) (x : EuclideanSpace' d) (h : x ∉ E) : c * EReal.indicator E x = 0

Indicator function evaluates to 0 if x ∉ E

noncomputable def UnsignedSimpleFunction.IntegralWellDef.weightedMeasureSum {d k : ℕ} (c : Fin k → EReal) (E : Fin k → Set (EuclideanSpace' d)) : EReal

The weighted measure sum for a representation

Equations

• UnsignedSimpleFunction.IntegralWellDef.weightedMeasureSum c E = ∑ i : Fin k, c i * Lebesgue_measure (E i)

theorem UnsignedSimpleFunction.IntegralWellDef.weightedMeasureSum_eq_of_eq {d k k' : ℕ} {c : Fin k → EReal} {E : Fin k → Set (EuclideanSpace' d)} {c' : Fin k' → EReal} {E' : Fin k' → Set (EuclideanSpace' d)} (hmes : ∀ (i : Fin k), LebesgueMeasurable (E i)) (hmes' : ∀ (i : Fin k'), LebesgueMeasurable (E' i)) (hnonneg : ∀ (i : Fin k), c i ≥ 0) (hnonneg' : ∀ (i : Fin k'), c' i ≥ 0) (heq : ∑ i : Fin k, c i • EReal.indicator (E i) = ∑ i : Fin k', c' i • EReal.indicator (E' i)) : weightedMeasureSum c E = weightedMeasureSum c' E'

Core lemma: Two representations of the same function give the same weighted measure sum. This is the heart of Lemma 1.3.4 (Venn diagram argument).

Single-family atoms (k' = 0 specialization)

When working with a single family of sets (no second family to compare against), we specialize the atom machinery with k' = 0.

def UnsignedSimpleFunction.IntegralWellDef.singleAtom {X : Type u_1} {k : ℕ} (E : Fin k → Set X) (n : Fin (2 ^ k)) : Set X

The atom for a single family of sets, using k' = 0 in the general atom definition

Equations

• UnsignedSimpleFunction.IntegralWellDef.singleAtom E n = UnsignedSimpleFunction.IntegralWellDef.atom E (fun (x : Fin 0) => ∅) ⟨↑n, ⋯⟩

theorem UnsignedSimpleFunction.IntegralWellDef.singleAtom_pairwiseDisjoint {X : Type u_1} {k : ℕ} (E : Fin k → Set X) : Set.univ.PairwiseDisjoint (singleAtom E)

Single atoms are pairwise disjoint

theorem UnsignedSimpleFunction.IntegralWellDef.mem_singleAtom_iff {X : Type u_1} {k : ℕ} (E : Fin k → Set X) (n : Fin (2 ^ k)) (x : X) : x ∈ singleAtom E n ↔ ∀ (i : Fin k), (↑n).testBit ↑i = true ↔ x ∈ E i

Membership in singleAtom is determined by bit pattern

theorem UnsignedSimpleFunction.IntegralWellDef.exists_unique_singleAtom {X : Type u_1} [DecidableEq X] {k : ℕ} (E : Fin k → Set X) (x : X) : ∃! n : Fin (2 ^ k), x ∈ singleAtom E n

Every point is in exactly one singleAtom

noncomputable def UnsignedSimpleFunction.IntegralWellDef.atomValue {k : ℕ} (c : Fin k → ℝ) (n : Fin (2 ^ k)) : ℝ

The value on atom n is the sum of coefficients for sets containing that atom

Equations

• UnsignedSimpleFunction.IntegralWellDef.atomValue c n = ∑ i : Fin k, if (↑n).testBit ↑i = true then c i else 0

theorem UnsignedSimpleFunction.integral_eq {d : ℕ} {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 k, c i * Lebesgue_measure (E 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 AlmostEverywhereEqual.refl {d : ℕ} {X : Type u_1} (f : EuclideanSpace' d → X) : AlmostEverywhereEqual f f

Almost everywhere equality is reflexive

theorem AlmostEverywhereEqual.symm {d : ℕ} {X : Type u_1} {f g : EuclideanSpace' d → X} (h : AlmostEverywhereEqual f g) : AlmostEverywhereEqual g f

Almost everywhere equality is symmetric

theorem AlmostEverywhereEqual.trans {d : ℕ} {X : Type u_1} {f g h : EuclideanSpace' d → X} (hfg : AlmostEverywhereEqual f g) (hgh : AlmostEverywhereEqual g h) : AlmostEverywhereEqual f h

Almost everywhere equality is transitive

theorem AlmostEverywhereEqual.equivalence {d : ℕ} {X : Type u_1} : Equivalence AlmostEverywhereEqual

Almost everywhere equality is an equivalence relation

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

Disjoint representation for RealSimpleFunction

Measure-theory specific lemmas for the disjoint representation of simple functions.

theorem RealSimpleFunction.DisjointRepr.singleAtom_measurable {d k : ℕ} {E : Fin k → Set (EuclideanSpace' d)} (hE : ∀ (i : Fin k), LebesgueMeasurable (E i)) (n : Fin (2 ^ k)) : LebesgueMeasurable (UnsignedSimpleFunction.IntegralWellDef.singleAtom E n)

Single atoms are measurable

theorem RealSimpleFunction.DisjointRepr.sum_indicator_eq_atomValue {d k : ℕ} (c : Fin k → ℝ) (E : Fin k → Set (EuclideanSpace' d)) (n : Fin (2 ^ k)) (x : EuclideanSpace' d) (hx : x ∈ UnsignedSimpleFunction.IntegralWellDef.singleAtom E n) : ∑ i : Fin k, c i * (E i).indicator' x = UnsignedSimpleFunction.IntegralWellDef.atomValue c n

On a point in singleAtom n, the original sum equals atomValue n

theorem RealSimpleFunction.DisjointRepr.eq_sum_atomValue_indicator {d k : ℕ} (c : Fin k → ℝ) (E : Fin k → Set (EuclideanSpace' d)) : ∑ i : Fin k, c i • (E i).indicator' = ∑ n : Fin (2 ^ k), UnsignedSimpleFunction.IntegralWellDef.atomValue c n • (UnsignedSimpleFunction.IntegralWellDef.singleAtom E n).indicator'

The original function equals the sum over atoms with atomValue coefficients

theorem RealSimpleFunction.disjoint_representation {d : ℕ} {f : EuclideanSpace' d → ℝ} (hf : RealSimpleFunction f) : ∃ (n : ℕ) (v : Fin n → ℝ) (A : Fin n → Set (EuclideanSpace' d)), (∀ (i : Fin n), LebesgueMeasurable (A i)) ∧ Set.univ.PairwiseDisjoint A ∧ f = ∑ i : Fin n, v i • (A i).indicator'

Disjoint representation: any RealSimpleFunction has an equivalent representation with pairwise disjoint, measurable sets.

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