TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every nonnegative measurable function admits an explicit increasing sequence of simple approximations

Statement

Let $(X, A)$ be a measurable space and let $f : X \to [0, + \infty]$ be measurable. For $k \in N$ define

$s_{k} : = \sum_{j = 0}^{k 2^{k} - 1} j 2^{- k} 1_{{j 2^{- k} \leq f < (j + 1) 2^{- k}}} + k 1_{{f \geq k}} .$

Then each $s_{k}$ is a simple measurable function,

$0 \leq s_{k} \leq s_{k + 1} \leq f,$

and $s_{k} (x) \to f (x)$ for every $x \in X$ . If $E \subseteq X$ is a set on which $f \leq M < + \infty$ , then $s_{k} \to f$ uniformly on $E$ .

Facts & Assumptions

Given: A measurable space $(X, A)$ , a measurable function $f : X \to [0, + \infty]$ , and the dyadic truncations $s_{k}$ displayed above.

[L1]

Threshold measurability characterizes measurable $\overline{R}$ -valued functions. (Threshold characterisations of real-valued and extended-real-valued measurability)

[L2]

A measurable real-valued function with finite range is simple, and its canonical representation is the sum over its level sets. (A simple function and its canonical representation)

Proof

technique · direct

1.1L1L2

For fixed $k$ , each set [L1, L2] ${j 2^{- k} \leq f < (j + 1) 2^{- k}}$ and ${f \geq k}$ is measurable by [L1]. Hence $s_{k}$ is a measurable real-valued function. Its values belong to the finite set ${0, 2^{- k}, 2 \cdot 2^{- k}, \dots, (k 2^{k} - 1) 2^{- k}, k}$ , so [L2] makes $s_{k}$ a simple function.

1.2givenalgebra

Fix $x \in X$ . If $f (x) \geq k$ , then $s_{k} (x) = k \leq f (x)$ and also [given, algebra] $s_{k + 1} (x) \geq k = s_{k} (x)$ . If $f (x) < k$ , choose $j$ with $j 2^{- k} \leq f (x) < (j + 1) 2^{- k}$ . Then $s_{k} (x) = j 2^{- k} \leq f (x)$ and $f (x) - s_{k} (x) < 2^{- k}$ . At the finer scale $2^{- k - 1}$ , the same point lies in one of the two adjacent dyadic cells over that coarse cell, so $s_{k + 1} (x)$ is either $j 2^{- k}$ or $j 2^{- k} + 2^{- k - 1}$ . Thus $s_{k} (x) \leq s_{k + 1} (x) \leq f (x)$ .

2.1step 1.2

The inequalities of step 1.2 hold for every $x$ , so [step 1.2] $0 \leq s_{k} \leq s_{k + 1} \leq f$ . If $f (x) < + \infty$ , then for all $k > f (x)$ the second case of step 1.2 applies and gives $0 \leq f (x) - s_{k} (x) < 2^{- k}$ , hence $s_{k} (x) \to f (x)$ . If $f (x) = + \infty$ , then $s_{k} (x) = k$ for every $k$ , so $s_{k} (x) \to + \infty = f (x)$ .

3.1

If $f \leq M < + \infty$ on a set $E$ , then for every $k > M$ the second case of [step 1.2, step 2.1] step 1.2 applies to every $x \in E$ and gives $0 \leq f (x) - s_{k} (x) < 2^{- k}$ . Therefore

$\sup_{x \in E} ∣ f (x) - s_{k} (x) ∣ \leq 2^{- k},$

so $s_{k} \to f$ uniformly on $E$ . [step 1.2, step 2.1] ∎

Depends on

Used by

Dependency tree · two levels

6 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Sheldon Axler, Measure, Integration and Real Analysis, Theorem 2.89 (standard reference, not scraped)