298 CHAPTER 10. THE ABSTRACT LEBESGUE INTEGRAL

Proof: By Theorem 9.1.6 on Page 239 there exists an increasing sequence of nonnega-tive simple functions, {sn} which converges pointwise to f . By the monotone convergencetheorem and Lemma 10.11.2,∫

φ ( f )dµ = limn→∞

∫φ (sn)dµ = lim

n→∞

∫∞

0φ′ (t)µ ([sn > t])dm

=∫

∞

0φ′ (t)µ ([ f > t])dm ■

This theorem can be generalized to a situation in which φ is only increasing and con-tinuous. In the generalization I will replace the symbol φ with F to coincide with earliernotation.

The following lemma and theorem say essentially that for F an increasing functionequal to 0 at 0,

∫(0,∞] µ ([ f > t])dF =

∫Ω

F ( f )dµ . I think it is particularly memorable ifF is differentiable when it looks like what was just discussed.

∫(0,∞] µ ([ f > t])F ′ (t)dt =∫

ΩF ( f )dµ

Lemma 10.11.5 Suppose s≥ 0 is a simple function, s(ω)≡∑nk=1 akXEk (ω) where the

ak are the distinct nonzero values of s,a1 < a2 < · · · < an. Suppose F is an increasingfunction defined on [0,∞),F (0) = 0,F being continuous at 0 from the right and continuousat every ak. Then letting µ be a measure and (Ω,F ,µ) a measure space,∫

(0,∞]µ ([s > t])dν =

∫Ω

F (s)dµ.

where the integral on the left is the Lebesgue integral for the Lebesgue Stieltjes measure ν

which comes from the increasing function F as in Theorem 10.10.1 above.

Proof: This follows from the following computation. Since F is continuous at 0 andthe values ak, ∫

∞

0µ ([s > t])dν (t) =

n

∑k=1

∫(ak−1,ak]

µ ([s > t])dν (t)

=n

∑k=1

∫(ak−1,ak]

n

∑j=k

µ (E j)dF (t) =n

∑j=1

µ (E j)j

∑k=1

ν ((ak−1,ak])

=n

∑j=1

µ (E j)j

∑k=1

(F (ak)−F (ak−1)) =n

∑j=1

µ (E j)F (a j)≡∫

Ω

F (s)dµ ■

Now here is the generalization to nonnegative measurable f .

Theorem 10.11.6 Let f ≥ 0 be measurable with respect to F , (Ω,F ,µ) a mea-sure space, and let F be an increasing continuous function defined on [0,∞) and F (0) = 0.Then

∫Ω

F ( f )dµ =∫(0,∞] µ ([ f > t])dν (t) where ν is the Lebesgue Stieltjes measure de-

termined by F as in Theorem 10.10.1 above.

Proof: By Theorem 9.1.6 on Page 239 there exists an increasing sequence of nonnega-tive simple functions, {sn} which converges pointwise to f . By the monotone convergencetheorem and Lemma 10.11.5,∫

Ω

F ( f )dµ = limn→∞

∫Ω

F (sn)dµ = limn→∞

∫(0,∞]

µ ([sn > t])dν =∫(0,∞]

µ ([ f > t])dν ■