LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

The layer-cake identity for integrable functions

Statement

Assume the Axiom of Countable Choice. Let $(X, A, μ)$ be any measure space, and let $f, g \in L^{1} (X)$ be nonnegative integrable functions with fixed pointwise nonnegative measurable representatives. For $t > 0$ put $E_{t} : = {x \in X : f (x) \geq t}$ and $E_{t}^{'} : = {x \in X : g (x) \geq t}$ , and let $d t$ denote Lebesgue measure on the level parameter. Then $∥ f - g ∥_{1} = \int_{0}^{\infty} μ (E_{t} △ E_{t}^{'}) d t,$ and in particular $∥ f ∥_{1} = \int_{0}^{\infty} μ (E_{t}) d t .$ No $σ$ -finiteness of $μ$ is required: both integrands are supported on $S : = {x : f (x) + g (x) > 0}$ , which is $σ$ -finite.

Facts & Assumptions

Given: The Axiom of Countable Choice, a measure space $(X, A, μ)$ , and nonnegative $L^{1}$ classes with the fixed representatives in the statement.

[A1]

The Axiom of Countable Choice is the assumption used to construct the library's Lebesgue measure on $R$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

$L^{1} (μ)$ is a real vector space, its quotient $L^{1} (μ)$ uses almost-everywhere classes, and its norm is the integral of the absolute value (The function space $L^{p} (μ)$ for $0 < p < \infty$ , The space $L^{p} (μ)$ as the quotient by null functions, $L^{p}$ and $L^{\infty}$ are vector spaces for $p \geq 1$ ).

[F2]

For a nonnegative measurable $h$ and $a > 0$ , $μ ({h \geq a}) \leq a^{- 1} \int h d μ$ (Chebyshev-Markov inequality for the integral).

[F3]

Under [A1], Lebesgue measure $λ$ on $R$ is a measure, is $σ$ -finite, and assigns length $b - a$ to each interval $(a, b]$ (Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume, Lebesgue measure is sigma-finite, and every metrically bounded subset of $R^{n}$ has finite outer measure, A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included, Finite, sigma-finite, and semifinite measures).

[F4]

The rationals are countable and dense in $R$ , and for every $ε > 0$ some $n \in N$ has $1 / n < ε$ ( $Q$ is countably infinite, Every subset of an at most countable set is at most countable, Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable, For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , The natural numbers $N$ (von Neumann)).

[F5]

Product-measurable rectangles, countable unions and intersections are measurable; product measure is defined for $σ$ -finite measure spaces and Tonelli's theorem interchanges the integrals of a nonnegative product-measurable function on such a product (Sigma-algebras, A measurable function between measurable spaces, The Borel sigma-algebra of a topological space, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, The product measure of two sigma-finite measure spaces, Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

Proof

technique · direct

1.1F1F2F4

Put $h : = f + g$ and $S : = {x : h (x) > 0}$ . By [F1], $h \in L^{1} (μ)$ and $\int h d μ < \infty$ . For each $n \geq 1$ , $S_{n} : = {x : h (x) \geq 1 / n}$ is measurable and [F2] gives $μ (S_{n}) \leq n \int h d μ < \infty$ . The sets $S_{n}$ cover $S$ : if $h (x) > 0$ , [F4] gives $n$ with $1 / n < h (x)$ . Thus $S$ is $σ$ -finite with its restricted measure, and $f = g = 0$ on $X ∖ S$ .

1.2F3F4F5algebra

For $f$ , define $A_{f} : = {(x, t) \in S \times R : 0 < t \leq f (x)}$ . Countability of $Q_{> 0}$ and [F5] make $A_{f} = ⋂_{m \geq 1} ⋃_{q \in Q_{> 0}} ((S \cap {x : f (x) > q}) \times (0, q + 1 / m])$ product-measurable. Indeed, if $0 < t \leq f (x)$ , density of $Q$ supplies for each fixed $m$ a rational $q$ with $\max (0, t - 1 / m) < q < f (x)$ , so $t \leq q + 1 / m$ . Conversely, membership in every union gives $f (x) > t - 1 / m$ for each $m$ ; if $f (x) < t$ , [F4] gives $m$ with $1 / m < t - f (x)$ , a contradiction. Define $A_{g}$ in the same way and put $D : = A_{f} △ A_{g}$ . For each $t > 0$ , its section is $E_{t} △ E_{t}^{'}$ , while for each $x \in S$ its section is $(0, f (x)] △ (0, g (x)]$ , whose Lebesgue measure is $∣ f (x) - g (x) ∣$ by [F3].

2.1A1F1F3F5step 1.1step 1.2

The restricted measure $μ ∣_{S}$ is $σ$ -finite by step 1.1, and $λ$ is $σ$ -finite by [F3], so [F5] applies to $1_{D}$ on their product. Since $D \subseteq S \times (0, \infty)$ and $f = g = 0$ off $S$ , Tonelli gives $∥ f - g ∥_{1} = \int_{S} ∣ f - g ∣ d μ = \int_{S} \int_{R} 1_{D} (x, t) d λ (t) d μ (x) = \int_{R} \int_{S} 1_{D} (x, t) d μ (x) d λ (t) = \int_{0}^{\infty} μ (E_{t} △ E_{t}^{'}) d t$ .

3.1step 2.1∎

Taking $g = 0$ in step 2.1 gives $∥ f ∥_{1} = \int_{0}^{\infty} μ (E_{t}) d t$ . The only choice assumption used is [A1]; the reduction from $X$ to $S$ and the countable product-measurability description are explicit.

Depends on

Used by

Dependency tree · two levels

123 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

Bachir Bekka, Pierre de la Harpe and Alain Valette, Kazhdan's Property (T) (standard reference, not scraped)
Anne Thomas, The Banach-Tarski Paradox and Amenability, Lecture 19: Reiter's Property and the Følner Condition (standard reference, not scraped)