TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

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.

Cauchy sequences in measure converge in measure

Statement

Let $(X, A, μ)$ be a measure space and let $f_{n} : X \to R$ be measurable. If $(f_{n})$ is Cauchy in measure, then there is a measurable $f : X \to R$ such that $f_{n} \to f$ in measure.

Facts & Assumptions

Given: A measure space $(X, A, μ)$ and a measurable sequence $f_{n} : X \to R$ that is Cauchy in measure.

[L1]

Cauchy in measure means that for every real $ε > 0$ and every $η > 0$ there is $N$ such that $m, n \geq N \Rightarrow μ ({∣ f_{n} - f_{m} ∣ > ε}) < η$ . (Cauchy sequences in measure)

[L2]

For measurable $(E_{k})$ one has $μ (⋃_{k} E_{k}) \leq \sum_{k = 0}^{\infty} μ (E_{k})$ . (Finite and countable subadditivity of measures)

[L3]

If $(E_{r})$ is a decreasing sequence of measurable sets and one $E_{r_{0}}$ has finite measure, then $μ (⋂_{r} E_{r}) = \inf_{r} μ (E_{r})$ . (Continuity from above when one set has finite measure)

[L4]

A uniformly Cauchy sequence of real-valued functions on a set converges uniformly to some real-valued function on that set. (A sequence of real-valued functions converges uniformly if and only if it is uniformly Cauchy)

[L5]

For a measurable set $E$ , the indicator $1_{E}$ is measurable. (An indicator function is measurable exactly when its set is measurable)

[L6]

Products of measurable real-valued functions are measurable. (Arithmetic and lattice operations preserve measurability whenever they are defined)

[L7]

Pointwise limits of measurable functions are measurable. (Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable)

[L8]

Convergence in measure means that for every real $ε > 0$ , $μ ({∣ f_{n} - f ∣ > ε}) \to 0$ . (Convergence in measure)

Proof

technique · direct

1.1

For each $k \geq 0$ , [L1] with $ε = η = 2^{- (k + 1)}$ gives an index $N_{k}$ such that $m, n \geq N_{k} ⟹ μ ({∣ f_{n} - f_{m} ∣ > 2^{- (k + 1)}}) < 2^{- (k + 1)} .$ Choose a strictly increasing sequence $(n_{k})_{k \geq 0}$ with $n_{k} \geq N_{k}$ for every $k$ . Then $n \geq n_{k} ⟹ μ ({∣ f_{n} - f_{n_{k}} ∣ > 2^{- (k + 1)}}) < 2^{- (k + 1)} .$

L1choose

2.1

For $k \geq 0$ put $A_{k} : = {∣ f_{n_{k + 1}} - f_{n_{k}} ∣ > 2^{- (k + 1)}}$ , $E_{r} : = ⋃_{k \geq r} A_{k}$ , and $G_{r} : = X ∖ E_{r}$ . Step 1.1 gives $μ (A_{k}) < 2^{- (k + 1)}$ , so $μ (E_{r}) \leq \sum_{k = r}^{\infty} 2^{- (k + 1)} = 2^{- r} .$ Thus $μ (E_{0}) \leq 1 < + \infty$ , the sets $E_{r}$ decrease with $r$ , and [L3] gives $μ ⁣ (⋂_{r = 0}^{\infty} E_{r}) = 0.$ Call this null set $N$ .

step 1.1L2L3algebra

3.1

Fix $r \geq 0$ . If $x \in G_{r}$ and $m > ℓ \geq r$ , then $x \notin A_{j}$ for every $j \geq r$ , so $∣ f_{n_{j + 1}} (x) - f_{n_{j}} (x) ∣ \leq 2^{- (j + 1)}$ for $j = ℓ, \dots, m - 1$ . Therefore $∣ f_{n_{m}} (x) - f_{n_{ℓ}} (x) ∣ \leq \sum_{j = ℓ}^{m - 1} 2^{- (j + 1)} \leq 2^{- ℓ} .$ Hence the tail $(f_{n_{k}} ∣_{G_{r}})_{k \geq r}$ is uniformly Cauchy on $G_{r}$ , so [L4] gives a function $g_{r} : G_{r} \to R$ with $f_{n_{k}} ∣_{G_{r}} \to g_{r}$ uniformly on $G_{r}$ .

step 2.1L4algebra

4.1

By [L5], $1_{G_{r}}$ is measurable. Since each $f_{n_{k}}$ is measurable, [L6] makes $u_{k, r} : = f_{n_{k}} 1_{G_{r}}$ measurable on $X$ . For $x \in G_{r}$ one has $u_{k, r} (x) = f_{n_{k}} (x) \to g_{r} (x)$ , while for $x \notin G_{r}$ all $u_{k, r} (x) = 0$ . So [L7] gives a measurable function $h_{r} : X \to R$ such that $h_{r} = g_{r}$ on $G_{r}$ and $h_{r} = 0$ on $E_{r}$ . The sets $G_{r}$ increase and cover $X ∖ N$ , and on overlaps the limits agree, so $(h_{r} (x))_{r \geq 0}$ stabilizes for every $x$ . Define $f (x) : = \lim_{r \to \infty} h_{r} (x) .$ By [L7] again, $f$ is measurable.

step 3.1L5L6L7construct

5.1

Fix $k \geq 0$ and $n \geq n_{k}$ . If $x \in G_{k}$ , then step 4.1 makes $f (x) = g_{k} (x)$ , so letting $m \to \infty$ in step 3.1 with $ℓ = k$ gives $∣ f_{n_{k}} (x) - f (x) ∣ \leq 2^{- k}$ . Hence on $G_{k}$ , $∣ f_{n} (x) - f (x) ∣ \leq ∣ f_{n} (x) - f_{n_{k}} (x) ∣ + 2^{- k} .$ Therefore ${∣ f_{n} - f ∣ > 3 \cdot 2^{- (k + 1)}} \subseteq {∣ f_{n} - f_{n_{k}} ∣ > 2^{- (k + 1)}} \cup E_{k} .$ Step 1.1 makes the first set have measure below $2^{- (k + 1)}$ , and step 2.1 gives $μ (E_{k}) \leq 2^{- k}$ . So $μ ({∣ f_{n} - f ∣ > 3 \cdot 2^{- (k + 1)}}) < 3 \cdot 2^{- (k + 1)} (n \geq n_{k}) .$

step 1.1step 2.1step 3.1step 4.1algebra

6.1

Given $ε, η > 0$ , choose $k$ with $3 \cdot 2^{- (k + 1)} < \min {ε, η}$ . Then for $n \geq n_{k}$ , $μ ({∣ f_{n} - f ∣ > ε}) \leq μ ({∣ f_{n} - f ∣ > 3 \cdot 2^{- (k + 1)}}) < η .$ This is exactly [L8].

step 5.1L8choose

7.1

The measurable function $f$ from step 4.1 is the limit of $(f_{n})$ in measure.

step 4.1step 6.1L8∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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

Gerald B. Folland, Real Analysis, 2nd ed., Theorem 2.30 (standard reference, not scraped)