Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-31
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 finite signed or complex measure has a polar decomposition against its total variation

Statement

Let ν be a finite signed measure or a finite complex measure on (X,A). Then there exists a measurable function h such that ν(E)=∫Eh d∣ν∣(E∈A),∣h∣=1∣ν∣-almost everywhere. If ν is signed, then h may be chosen real-valued, and for a Hahn decomposition X=P⊔N one may take h=χP−χN∣ν∣-almost everywhere.

Facts & Assumptions

Given: A finite signed or finite complex measure ν.

[L1]

For every measurable set E, one has ∣ν(E)∣≤∣ν∣(E), so ν≪∣ν∣; finite signed measures therefore admit Radon-Nikodym densities with respect to ∣ν∣ by the signed theorem, and finite complex measures do so by the complex corollary. (The total variation |nu|(E) from countable measurable partitions, The Radon-Nikodym derivative as an almost-everywhere equivalence class, A sigma-finite signed measure that is absolutely continuous with respect to a sigma-finite positive measure has a unique almost-everywhere density, A finite complex measure absolutely continuous with respect to a sigma-finite positive measure has an integrable complex density)

[L2]

For an absolutely continuous finite signed or finite complex measure, the total variation has density equal to the modulus of the Radon-Nikodym derivative. (The total variation of an absolutely continuous signed or complex measure has density the absolute value of the Radon-Nikodym derivative)

[L3]

A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere. (A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere)

[L4]

In the signed case, a Hahn decomposition X=P⊔N exists, and on its positive and negative pieces the Jordan and total-variation formulas give ν=∣ν∣ and ν=−∣ν∣, respectively (Hahn decomposition for signed measures, unique up to total-variation-null sets, Jordan decomposition of a signed measure into unique mutually singular positive parts, For a signed measure, total variation is nu-plus plus nu-minus, finite partitions suffice, and nu-plus and nu-minus are extremal).

Proof

technique · direct
1.1

Because ∣ν(E)∣≤∣ν∣(E) for every measurable E, the measure ν is absolutely continuous with respect to ∣ν∣. Thus [L1] gives a density h=dν/d∣ν∣ with ν(E)=∫Eh d∣ν∣(E∈A).

L1given
2.1

Apply [L2] with μ:=∣ν∣. Then ∣ν∣(E)=∫E∣h∣ d∣ν∣(E∈A). Let A:={∣h∣>1}. Using the displayed identity on A gives 0=∫A∣h∣ d∣ν∣−∣ν∣(A)=∫A(∣h∣−1) d∣ν∣. Because ∣h∣−1≥0 on A, [L3] yields ∣ν∣(A)=0. Now let B:={∣h∣<1}. Since A is ∣ν∣-null, 0=∣ν∣(B)−∫B∣h∣ d∣ν∣=∫B(1−∣h∣) d∣ν∣. Again the integrand is nonnegative, so [L3] gives ∣ν∣(B)=0. Therefore ∣h∣=1 ∣ν∣-almost everywhere.

step 1.1L2L3algebra
3.1

If ν is signed, let X=P⊔N be a Hahn decomposition from [L4]. Then χP−χN is real-valued and has modulus 1 everywhere. For every measurable E, additivity and the Jordan formulas give ν(E)=ν(E∩P)+ν(E∩N)=∣ν∣(E∩P)−∣ν∣(E∩N)=∫E(χP−χN) d∣ν∣. Hence the signed case may be represented by h=χP−χN.

L4step 2.1algebra
4.1

Steps 1.1, 2.1, and 3.1 prove the general polar decomposition and the signed specialization.

step 1.1step 2.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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