Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-09 (gpt-6-astra)
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.

A sigma-finite signed measure that is absolutely continuous with respect to a sigma-finite positive measure has a unique almost-everywhere density

Statement

Assume the Axiom of Choice. Let μ be a positive measure and let ν be a signed measure on (X,A). Assume there is an increasing measurable exhaustion (Xn) with ⋃nXn=X, μ(Xn)<+∞, and ∣ν∣(Xn)<+∞ for every n. If ν≪μ, then there exists a measurable real-valued function f, unique up to μ-almost-everywhere equality, such that ν(E)=∫Ef dμ(E∈A). If in addition ∣ν∣(X)<+∞, then f∈L1(μ).

Facts & Assumptions

Given: AC, a positive measure μ, a signed measure ν with a common finite exhaustion (Xn), and the hypothesis ν≪μ.

[L1]

The Lebesgue decomposition theorem gives ν=νa+νs with νa≪μ, νs⊥μ, and νa(E)=∫Ef dμ for every measurable E, with f real-valued and ∫Xn∣f∣ dμ<∞. (Every sigma-finite signed measure admits a Lebesgue decomposition relative to a sigma-finite positive measure)

[L2]

A signed or complex measure that is both absolutely continuous and singular with respect to μ is zero. (A signed or complex measure that is both absolutely continuous and singular with respect to the same positive measure is zero)

[L3]

Real integrability means finiteness of both positive and negative integrals; the integral is linear on L1. (Integrable real and complex functions, and their integrals, The Lebesgue integral is linear on L1(μ))

[L5]

Variation dominates ∣ν(E)∣ by its partition definition. (The total variation |nu|(E) from countable measurable partitions)

[L4]

AC is assumed for the selections in [L1]. (The Axiom of Choice)

Proof

technique · direct
1.1L1choose

By [L1], write ν=νa+νs, where νa≪μ, νs⊥μ, and νa(E)=∫Ef dμ for every measurable E, with f real-valued and ∫Xn∣f∣ dμ<∞.

2.1step 1.1L2algebra

Because ν≪μ and νa≪μ, on each μ-null set E the decomposition gives 0=0+νs(E), so νs≪μ without subtracting infinite values. Step 1.1 already gives νs⊥μ, so [L2] forces νs=0. Hence ν=νa, and the displayed integral formula for f represents ν on every measurable set.

3.1step 2.1choosealgebra

Suppose g is another measurable real-valued function with ν(E)=∫Eg dμ for every measurable E. Fix n. The formula on Xn gives ∫Xng dμ=ν(Xn)∈R, so both positive and negative integrals of g there are finite. Thus f,g∈L1(Xn), and [L3] permits subtraction of their integrals over every measurable subset of Xn. For each m≥1, let Pn,m:=Xn∩{f−g≥1/m},Nn,m:=Xn∩{g−f≥1/m}. Applying the two representation formulas to Pn,m gives 0=∫Pn,m(f−g) dμ≥μ(Pn,m)/m, so μ(Pn,m)=0; the same argument with Nn,m gives μ(Nn,m)=0. Therefore Xn∩{f≠g}=⋃m≥1Pn,m∪⋃m≥1Nn,m is μ-null. Since X=⋃nXn, the functions f and g agree μ-almost everywhere on X.

3.2L3step 2.1algebra

If ∣ν∣(X)<∞, use the representation on the measurable sets P={f≥0} and N={f<0}. It gives ∫f+ dμ=ν(P) and ∫f− dμ=−ν(N). Both are finite: ∣ν(E)∣≤∣ν∣(X) for every E, directly from the partition definition of variation. Hence f∈L1(μ) by [L3].

4.1step 2.1step 3.1step 3.2∎

Steps 2.1, 3.1, and 3.2 prove existence, almost-everywhere uniqueness, and the finite-measure integrability clause.

Depends on

Used by

Dependency tree · two levels

28 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