def IsSimpleFunction {n : ℕ} (Ω : Set (Fin n → ℝ)) (f : ↑Ω → ℝ) : Prop

Definition 8.1 (Simple functions): for a function f : Ω → ℝ on a measurable-domain subset Ω ⊆ ℝ^n, being simple means Ω is measurable, f is measurable, and f takes only finitely many values (equivalently, f(Ω) is finite).

Equations

• IsSimpleFunction Ω f = (MeasurableSet Ω ∧ Measurable f ∧ (Set.range f).Finite)

theorem helperForLemma_8_1_range_add_subset_image_prod {n : ℕ} {Ω : Set (Fin n → ℝ)} (f g : ↑Ω → ℝ) : (Set.range fun (x : ↑Ω) => f x + g x) ⊆ (fun (p : ℝ × ℝ) => p.1 + p.2) '' Set.range f ×ˢ Set.range g

Helper for Lemma 8.1: the range of a pointwise sum is contained in the image of the sum-map on the product of ranges.

theorem helperForLemma_8_1_range_add_finite {n : ℕ} {Ω : Set (Fin n → ℝ)} (f g : ↑Ω → ℝ) (hf : (Set.range f).Finite) (hg : (Set.range g).Finite) : (Set.range fun (x : ↑Ω) => f x + g x).Finite

Helper for Lemma 8.1: finite range is preserved by pointwise addition.

theorem helperForLemma_8_1_range_constMul_finite {n : ℕ} {Ω : Set (Fin n → ℝ)} (f : ↑Ω → ℝ) (c : ℝ) (hf : (Set.range f).Finite) : (Set.range fun (x : ↑Ω) => c * f x).Finite

Helper for Lemma 8.1: finite range is preserved by scalar multiplication.

theorem IsSimpleFunction.add {n : ℕ} {Ω : Set (Fin n → ℝ)} {f g : ↑Ω → ℝ} (hf : IsSimpleFunction Ω f) (hg : IsSimpleFunction Ω g) : IsSimpleFunction Ω fun (x : ↑Ω) => f x + g x

Helper for Lemma 8.1: simple functions are closed under pointwise addition.

theorem IsSimpleFunction.const_mul {n : ℕ} {Ω : Set (Fin n → ℝ)} {f : ↑Ω → ℝ} (hf : IsSimpleFunction Ω f) (c : ℝ) : IsSimpleFunction Ω fun (x : ↑Ω) => c * f x

Helper for Lemma 8.1: simple functions are closed under real scalar multiplication.

theorem lemma_8_1 {n : ℕ} {Ω : Set (Fin n → ℝ)} {f g : ↑Ω → ℝ} (hf : IsSimpleFunction Ω f) (hg : IsSimpleFunction Ω g) : (IsSimpleFunction Ω fun (x : ↑Ω) => f x + g x) ∧ ∀ (c : ℝ), IsSimpleFunction Ω fun (x : ↑Ω) => c * f x

Lemma 8.1: simple functions are closed under pointwise addition and scalar multiplication.

noncomputable def characteristicFunction {n : ℕ} (Ω : Set (Fin n → ℝ)) (E : Set ↑Ω) : ↑Ω → ℝ

Definition 8.2 (Characteristic function): for a measurable set Ω ⊆ ℝ^n and a measurable subset E ⊆ Ω, the characteristic (indicator) function χ_E : Ω → ℝ is χ_E(x) = 1 for x ∈ E and χ_E(x) = 0 for x ∉ E.

Equations

• characteristicFunction Ω E x = if x ∈ E then 1 else 0

theorem helperForLemma_8_2_coeffIndexing_injective {n N : ℕ} {Ω : Set (Fin n → ℝ)} {f : ↑Ω → ℝ} (e : Fin N ≃ ↑(Set.range f)) : Function.Injective fun (i : Fin N) => ↑(e i)

Helper for Lemma 8.2: indexing coefficients by an equivalence with Fin N is injective after coercing from Set.range f to ℝ.

theorem helperForLemma_8_2_fiberSets_measurable_subset {n N : ℕ} {Ω : Set (Fin n → ℝ)} {f : ↑Ω → ℝ} (hΩ : MeasurableSet Ω) (hf_meas : Measurable f) (c : Fin N → ℝ) : (∀ (i : Fin N), MeasurableSet (Subtype.val '' (f ⁻¹' {c i}))) ∧ ∀ (i : Fin N), Subtype.val '' (f ⁻¹' {c i}) ⊆ Ω

Helper for Lemma 8.2: the ambient-space fibers of a measurable f : Ω → ℝ are measurable and lie inside Ω.

theorem helperForLemma_8_2_mem_fiberSet_iff {n N : ℕ} {Ω : Set (Fin n → ℝ)} {f : ↑Ω → ℝ} (c : Fin N → ℝ) {x : Fin n → ℝ} (hx : x ∈ Ω) (i : Fin N) : x ∈ Subtype.val '' (f ⁻¹' {c i}) ↔ f ⟨x, hx⟩ = c i

Helper for Lemma 8.2: for x ∈ Ω, membership in an ambient fiber is equivalent to the corresponding value equation for f.

theorem helperForLemma_8_2_pairwiseDisjoint_fiberSets {n N : ℕ} {Ω : Set (Fin n → ℝ)} {f : ↑Ω → ℝ} (c : Fin N → ℝ) (hc_inj : Function.Injective c) : Pairwise fun (i j : Fin N) => Disjoint (Subtype.val '' (f ⁻¹' {c i})) (Subtype.val '' (f ⁻¹' {c j}))

Helper for Lemma 8.2: distinct fibers of coefficient values are disjoint.

theorem helperForLemma_8_2_pointwise_sum_representation {n N : ℕ} {Ω : Set (Fin n → ℝ)} {f : ↑Ω → ℝ} (e : Fin N ≃ ↑(Set.range f)) {x : Fin n → ℝ} (hx : x ∈ Ω) : f ⟨x, hx⟩ = ∑ i : Fin N, ↑(e i) * (Subtype.val '' (f ⁻¹' {↑(e i)})).indicator (fun (x : Fin n → ℝ) => 1) x

Helper for Lemma 8.2: at each x ∈ Ω, the finite coefficient/indicator sum collapses to the unique index corresponding to the value f x.

theorem lemma_8_2 {n : ℕ} {Ω : Set (Fin n → ℝ)} {f : ↑Ω → ℝ} (hΩ : MeasurableSet Ω) (hf : IsSimpleFunction Ω f) : ∃ (N : ℕ) (c : Fin N → ℝ) (E : Fin N → Set (Fin n → ℝ)), (∀ (i : Fin N), MeasurableSet (E i)) ∧ (∀ (i : Fin N), E i ⊆ Ω) ∧ (Pairwise fun (i j : Fin N) => Disjoint (E i) (E j)) ∧ ∀ (x : Fin n → ℝ) (hx : x ∈ Ω), f ⟨x, hx⟩ = ∑ i : Fin N, c i * (E i).indicator (fun (x : Fin n → ℝ) => 1) x

Lemma 8.2: if f : Ω → ℝ is simple, then there are N : ℕ, coefficients c : Fin N → ℝ, and pairwise disjoint measurable sets E i ⊆ Ω such that f = ∑ i=1^N c_i χ_{E_i} on Ω.

In this file, IsSimpleFunction Ω f (Definition 8.1) already packages that Ω is measurable, f is measurable, and f has finite range; the book's phrase "simple, i.e. finitely many values" is used as shorthand.

def NonnegSimpleFunction {n : ℕ} (Ω : Set (Fin n → ℝ)) : Type

A non-negative simple real-valued function on Ω.

Equations

• NonnegSimpleFunction Ω = { f : ↑Ω → ℝ // IsSimpleFunction Ω f ∧ ∀ (x : ↑Ω), 0 ≤ f x }

noncomputable def lebesgueIntegralNonnegSimple {n : ℕ} {Ω : Set (Fin n → ℝ)} (f : NonnegSimpleFunction Ω) : ENNReal

Definition 8.3 (Lebesgue integral of a non-negative simple function): for f : Ω → [0, ∞) simple, define ∫_Ω f dm = ∑_{λ ∈ f(Ω), λ > 0} λ * m({x ∈ Ω | f x = λ}).

Equations

• lebesgueIntegralNonnegSimple f = ∑ r ∈ ⋯.toFinset with 0 < r, ENNReal.ofReal r * MeasureTheory.volume (Subtype.val '' (↑f ⁻¹' {r}))

theorem helperForProposition_8_1_1_integral_eq_zero_iff_forall_posFiber_zero {n : ℕ} {Ω : Set (Fin n → ℝ)} (f : NonnegSimpleFunction Ω) : ∑ r ∈ ⋯.toFinset with 0 < r, ENNReal.ofReal r * MeasureTheory.volume (Subtype.val '' (↑f ⁻¹' {r})) = 0 ↔ ∀ r ∈ {r ∈ ⋯.toFinset | 0 < r}, MeasureTheory.volume (Subtype.val '' (↑f ⁻¹' {r})) = 0

Helper for Proposition 8.1.1: the integral sum is zero exactly when each positive-value fiber has zero ambient volume.

theorem helperForProposition_8_1_1_posFiber_subset_nonzeroImage {n : ℕ} {Ω : Set (Fin n → ℝ)} (f : NonnegSimpleFunction Ω) {r : ℝ} (hr : r ∈ {t ∈ ⋯.toFinset | 0 < t}) : Subtype.val '' (↑f ⁻¹' {r}) ⊆ Subtype.val '' {x : ↑Ω | ↑f x ≠ 0}

Helper for Proposition 8.1.1: each positive-value fiber is contained in the ambient nonzero image of f.

theorem helperForProposition_8_1_1_nonzeroImage_subset_iUnion_posFibers {n : ℕ} {Ω : Set (Fin n → ℝ)} (f : NonnegSimpleFunction Ω) : Subtype.val '' {x : ↑Ω | ↑f x ≠ 0} ⊆ ⋃ r ∈ {t ∈ ⋯.toFinset | 0 < t}, Subtype.val '' (↑f ⁻¹' {r})

Helper for Proposition 8.1.1: every ambient nonzero point belongs to a positive-value fiber from the finite range of f.

theorem helperForProposition_8_1_1_union_volume_zero_of_fibers_zero {n : ℕ} (S : Finset ℝ) (F : ℝ → Set (Fin n → ℝ)) (hvol : ∀ r ∈ S, MeasureTheory.volume (F r) = 0) : MeasureTheory.volume (⋃ r ∈ S, F r) = 0

Helper for Proposition 8.1.1: a finite union has zero volume when each indexed piece has zero volume.

theorem lebesgueIntegralNonnegSimple_nonneg_le_top_and_eq_zero_iff {n : ℕ} {Ω : Set (Fin n → ℝ)} (f : NonnegSimpleFunction Ω) : 0 ≤ lebesgueIntegralNonnegSimple f ∧ lebesgueIntegralNonnegSimple f ≤ ⊤ ∧ (lebesgueIntegralNonnegSimple f = 0 ↔ MeasureTheory.volume (Subtype.val '' {x : ↑Ω | ↑f x ≠ 0}) = 0)

Proposition 8.1.1: for a non-negative simple function f on Ω, one has 0 ≤ ∫_Ω f dm ≤ ∞; moreover ∫_Ω f dm = 0 iff m({x ∈ Ω | f(x) ≠ 0}) = 0.

theorem helperForLemma_8_3_isSimple_toReal_eapprox {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩ : MeasurableSet Ω) {f : ↑Ω → ENNReal} (k : ℕ) : IsSimpleFunction Ω fun (x : ↑Ω) => ((MeasureTheory.SimpleFunc.eapprox f k) x).toReal

Helper for Lemma 8.3: each approximation x ↦ (eapprox f k x).toReal is a simple function on Ω.

theorem helperForLemma_8_3_nonneg_mono_toReal_eapprox {n : ℕ} {Ω : Set (Fin n → ℝ)} {f : ↑Ω → ENNReal} (k : ℕ) (x : ↑Ω) : 0 ≤ ((MeasureTheory.SimpleFunc.eapprox f k) x).toReal ∧ ((MeasureTheory.SimpleFunc.eapprox f k) x).toReal ≤ ((MeasureTheory.SimpleFunc.eapprox f (k + 1)) x).toReal

Helper for Lemma 8.3: toReal ∘ eapprox is pointwise nonnegative and monotone in the approximation index.

theorem helperForLemma_8_3_ofReal_toReal_eapprox {n : ℕ} {Ω : Set (Fin n → ℝ)} {f : ↑Ω → ENNReal} (x : ↑Ω) (k : ℕ) : ENNReal.ofReal ((MeasureTheory.SimpleFunc.eapprox f k) x).toReal = (MeasureTheory.SimpleFunc.eapprox f k) x

Helper for Lemma 8.3: converting eapprox to ℝ and back with ofReal recovers the original ENNReal value.

theorem helperForLemma_8_3_tendsto_ofReal_toReal_eapprox {n : ℕ} {Ω : Set (Fin n → ℝ)} {f : ↑Ω → ENNReal} (hf : Measurable f) (x : ↑Ω) : Filter.Tendsto (fun (k : ℕ) => ENNReal.ofReal ((MeasureTheory.SimpleFunc.eapprox f k) x).toReal) Filter.atTop (nhds (f x))

Helper for Lemma 8.3: ENNReal.ofReal applied to toReal ∘ eapprox converges pointwise to f.

theorem lemma_8_3 {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩ : MeasurableSet Ω) {f : ↑Ω → ENNReal} (hf : Measurable f) : ∃ (fSeq : ℕ → ↑Ω → ℝ), (∀ (n_1 : ℕ), IsSimpleFunction Ω (fSeq n_1)) ∧ (∀ (n_1 : ℕ) (x : ↑Ω), 0 ≤ fSeq n_1 x ∧ fSeq n_1 x ≤ fSeq (n_1 + 1) x) ∧ ∀ (x : ↑Ω), Filter.Tendsto (fun (n : ℕ) => ENNReal.ofReal (fSeq n x)) Filter.atTop (nhds (f x))

Lemma 8.3: if Ω ⊆ ℝ^n is measurable and f : Ω → [0, +∞] is measurable, then there exists a sequence (f_n) of nonnegative simple functions f_n : Ω → ℝ such that (i) 0 ≤ f_n ≤ f_{n+1} pointwise, and (ii) for every x ∈ Ω, f_n x converges to f x in [0, +∞] (via ENNReal.ofReal).

theorem helperForLemma_8_4_sum_indicator_eq_zero_of_not_mem {n N : ℕ} {E : Fin N → Set (Fin n → ℝ)} (c : Fin N → ℝ) {x : Fin n → ℝ} (hx : ∀ (i : Fin N), x ∉ E i) : ∑ i : Fin N, c i * (E i).indicator (fun (x : Fin n → ℝ) => 1) x = 0

Helper for Lemma 8.4: if x lies in none of the sets E i, then the indicator expansion at x vanishes.

theorem helperForLemma_8_4_sum_indicator_eq_coeff_of_mem {n N : ℕ} {E : Fin N → Set (Fin n → ℝ)} (hE_disjoint : Pairwise fun (i j : Fin N) => Disjoint (E i) (E j)) (c : Fin N → ℝ) {x : Fin n → ℝ} {i : Fin N} (hxi : x ∈ E i) : ∑ j : Fin N, c j * (E j).indicator (fun (x : Fin n → ℝ) => 1) x = c i

Helper for Lemma 8.4: if x ∈ E i, pairwise disjointness makes the indicator expansion collapse to c i.

theorem helperForLemma_8_4_value_pos_fiber_iff_exists_index {n N : ℕ} {Ω : Set (Fin n → ℝ)} {E : Fin N → Set (Fin n → ℝ)} (hE_disjoint : Pairwise fun (i j : Fin N) => Disjoint (E i) (E j)) (c : Fin N → ℝ) (f : NonnegSimpleFunction Ω) (hf_repr : ∀ (x : Fin n → ℝ) (hx : x ∈ Ω), ↑f ⟨x, hx⟩ = ∑ i : Fin N, c i * (E i).indicator (fun (x : Fin n → ℝ) => 1) x) {r : ℝ} (hr_pos : 0 < r) {x : Fin n → ℝ} (hxΩ : x ∈ Ω) : x ∈ Subtype.val '' (↑f ⁻¹' {r}) ↔ ∃ (i : Fin N), x ∈ E i ∧ c i = r

Helper for Lemma 8.4: for positive r, membership in the r-fiber is equivalent to lying in some E i with coefficient c i = r.

theorem helperForLemma_8_4_measure_pos_fiber_as_filtered_sum {n N : ℕ} {Ω : Set (Fin n → ℝ)} {E : Fin N → Set (Fin n → ℝ)} (hE_meas : ∀ (i : Fin N), MeasurableSet (E i)) (hE_subset : ∀ (i : Fin N), E i ⊆ Ω) (hE_disjoint : Pairwise fun (i j : Fin N) => Disjoint (E i) (E j)) (c : Fin N → ℝ) (f : NonnegSimpleFunction Ω) (hf_repr : ∀ (x : Fin n → ℝ) (hx : x ∈ Ω), ↑f ⟨x, hx⟩ = ∑ i : Fin N, c i * (E i).indicator (fun (x : Fin n → ℝ) => 1) x) {r : ℝ} (hr_pos : 0 < r) : MeasureTheory.volume (Subtype.val '' (↑f ⁻¹' {r})) = ∑ i : Fin N with c i = r, MeasureTheory.volume (E i)

Helper for Lemma 8.4: each positive fiber has measure equal to the sum of the measures of those E i whose coefficients equal that value.

theorem helperForLemma_8_4_range_to_coeff_image_on_positive_part {n N : ℕ} {Ω : Set (Fin n → ℝ)} {E : Fin N → Set (Fin n → ℝ)} (hE_disjoint : Pairwise fun (i j : Fin N) => Disjoint (E i) (E j)) (c : Fin N → ℝ) (f : NonnegSimpleFunction Ω) (hf_repr : ∀ (x : Fin n → ℝ) (hx : x ∈ Ω), ↑f ⟨x, hx⟩ = ∑ i : Fin N, c i * (E i).indicator (fun (x : Fin n → ℝ) => 1) x) : ∑ r ∈ ⋯.toFinset with 0 < r, ENNReal.ofReal r * MeasureTheory.volume (Subtype.val '' (↑f ⁻¹' {r})) = ∑ r ∈ Finset.image c Finset.univ with 0 < r, ENNReal.ofReal r * MeasureTheory.volume (Subtype.val '' (↑f ⁻¹' {r}))

Helper for Lemma 8.4: replacing positive values in the range of f by positive values in the coefficient-image changes only zero terms.

theorem helperForLemma_8_4_reindex_double_sum_to_index_sum {n N : ℕ} (c : Fin N → ℝ) (hc_nonneg : ∀ (i : Fin N), 0 ≤ c i) (E : Fin N → Set (Fin n → ℝ)) : ∑ r ∈ Finset.image c Finset.univ with 0 < r, ENNReal.ofReal r * ∑ i : Fin N with c i = r, MeasureTheory.volume (E i) = ∑ i : Fin N, ENNReal.ofReal (c i) * MeasureTheory.volume (E i)

Helper for Lemma 8.4: regrouping the coefficient-filtered double sum gives the direct index-sum formula.

theorem lemma_8_4 {n N : ℕ} {Ω : Set (Fin n → ℝ)} (E : Fin N → Set (Fin n → ℝ)) (hE_meas : ∀ (i : Fin N), MeasurableSet (E i)) (hE_subset : ∀ (i : Fin N), E i ⊆ Ω) (hE_disjoint : Pairwise fun (i j : Fin N) => Disjoint (E i) (E j)) (c : Fin N → ℝ) (hc_nonneg : ∀ (i : Fin N), 0 ≤ c i) (f : NonnegSimpleFunction Ω) (hf_repr : ∀ (x : Fin n → ℝ) (hx : x ∈ Ω), ↑f ⟨x, hx⟩ = ∑ i : Fin N, c i * (E i).indicator (fun (x : Fin n → ℝ) => 1) x) : lebesgueIntegralNonnegSimple f = ∑ i : Fin N, ENNReal.ofReal (c i) * MeasureTheory.volume (E i)

Lemma 8.4: if a nonnegative simple function on Ω is represented by a finite pairwise-disjoint indicator expansion ∑ c_i χ_{E_i}, then its integral is ∑ c_i m(E_i).