9.10. THE DISTRIBUTION FUNCTION 217

9.10 The Distribution FunctionFor (Ω,F ,µ) a measure space, the integral of a nonnegative measurable function was de-fined earlier as

∫f dµ ≡

∫∞

0 µ ([ f > t])dt. This idea will be developed more in this section.

Definition 9.10.1 Let f ≥ 0 and suppose f is measurable. The distribution functionis the function defined by t→ µ ([t < f ]) .

Lemma 9.10.2 If { fn} is an increasing sequence of functions converging pointwise tof then µ ([ f > t]) = limn→∞ µ ([ fn > t]) .

Proof: The sets, [ fn > t] are increasing and their union is [ f > t] because if f (ω) > t,then for all n large enough, fn (ω)> t also. Therefore, the desired conclusion follows fromproperties of measures, the one which says that if En ↑ E, then µ (En) ↑ µ (E). ■

Note how it was important to have strict inequality in the definition.

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

ak are the distinct nonzero values of s,0 < a1 < a2 < · · · < an on the measurable sets Ek.Suppose φ is a C1 function defined on [0,∞) which has the properties that φ (0) = 0, andalso that φ

′ (t)> 0 for all t. Then∫∞

0φ′ (t)µ ([s > t])dm(t) =

∫φ (s)dµ (s) .

Proof: First note that if µ (Ek) = ∞ for any k then both sides equal ∞ and so withoutloss of generality, assume µ (Ek)< ∞ for all k. Letting a0 ≡ 0, the left side equals

n

∑k=1

∫ ak

ak−1

φ′ (t)µ ([s > t])dm(t) =

n

∑k=1

∫ ak

ak−1

φ′ (t)

n

∑i=k

µ (Ei)dm

=n

∑k=1

n

∑i=k

µ (Ei)∫ ak

ak−1

φ′ (t)dm =

n

∑k=1

n

∑i=k

µ (Ei)(φ (ak)−φ (ak−1))

=n

∑i=1

µ (Ei)i

∑k=1

(φ (ak)−φ (ak−1)) =n

∑i=1

µ (Ei)φ (ai) =∫

φ (s)dµ. ■

With this lemma the next theorem which is the main result follows easily.

Theorem 9.10.4 Let f ≥ 0 be measurable and let φ be a C1 function defined on[0,∞) which satisfies φ

′ (t)> 0 for all t > 0 and φ (0) = 0. Then∫φ ( f )dµ =

∫∞

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

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

φ ( f )dµ = limn→∞

∫φ (sn)dµ = lim

n→∞

∫∞

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

=∫

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

9.10. THE DISTRIBUTION FUNCTION 2179.10 The Distribution FunctionFor (Q,.¥, 1) a measure space, the integral of a nonnegative measurable function was de-fined earlier as { fdu = Jy WU ([f > t]) dt. This idea will be developed more in this section.Definition 9.10.1 Le: f =Oand suppose f is measurable. The distribution functionis the function defined by t > wu (|t < f]).Lemma 9.10.2 /f {f,} is an increasing sequence of functions converging pointwise tof then w ([f > t]) = limps Mt ([fn > ¢))-Proof: The sets, [f;, >t] are increasing and their union is [f > ft] because if f(@) >t,then for all n large enough, f, (@) >t also. Therefore, the desired conclusion follows fromproperties of measures, the one which says that if E, + £, then w(E,) tu (EZ).Note how it was important to have strict inequality in the definition.Lemma 9.10.3 Suppose s > 0 is a simple function, s(@) = Yi_, ax 2%, (@) where thea,x are the distinct nonzero values of s,0 < a, < dz < +++ <a, on the measurable sets Ex.Suppose @ is aC! function defined on |0,°) which has the properties that @ (0) = 0, andalso that 9’ (t) > 0 for all t. Then[ oxi ([s > ¢]) = [os s)du(sProof: First note that if u (£;) = ce for any k then both sides equal oo and so withoutloss of generality, assume pt (E,) < 0 for all k. Letting ap = 0, the left side equals¥ fH eomo>damo=¥ [" 9 Lucenak=17%-1 Jak ° i=kBhat t)dm = py Yue ~ 9 (ay-1))i=k aK}LE, DY @ (a1) =Yaue vo fou aWith this lemma the next theorem which is the main result follows easily.TM:>llunIllIMsanTheorem 9.10.4 Ler f > 0 be measurable and let @ be a C! function defined on(0,00) which satisfies $' (t) > 0 for all t > 0 and 9 (0) = 0. Then[onan= [oo ule > damProof: By Theorem 8.1.6 on Page 181 there exists an increasing sequence of nonnega-tive simple functions, {s,} which converges pointwise to f. By the monotone convergencetheorem and Lemma 9.10.2,[ocfaw = jim [6 (55) au = tim [9 0) (lon > al)[on ([f > t])dm