Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-30
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 complex measure has finite total variation

Statement

If ν is a complex measure on (X,A), then ν(X)<+. More generally, ν(E)<+ for every measurable E.

Facts & Assumptions

Given: A complex measure ν on (X,A) and a measurable set E.

[L1]

The total variation ν(E) is the supremum of the countable partition sums nν(En). (The total variation |nu|(E) from countable measurable partitions)

[L2]

The set functions α:=Reν and β:=Imν are finite signed measures and ν=α+iβ. (The real and imaginary parts of a complex measure are finite signed measures, and nu = Re nu + i Im nu)

[L3]

For a signed measure ρ with Jordan 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

Put α:=Reν and β:=Imν. By [L2], these are finite signed measures and ν(A)=α(A)+iβ(A)α(A)+β(A) for every measurable A.

L2algebra
2.1

Let (En) be any countable measurable partition of E. Step 1.1 and the one-piece lower bound in the definition of variation give nν(En)nα(En)+nβ(En)nα(En)+nβ(En). By [L3], α=α++α and β=β++β, so countable additivity of the four positive Jordan parts turns the right side into α(E)+β(E).

L1L3step 1.1
3.1

The quantities α(E) and β(E) are finite by [L2] and [L3]: both Jordan parts of a finite signed measure are finite on E. Thus step 2.1 gives the partition-independent bound nν(En)α(E)+β(E)<+. Taking the supremum over all countable measurable partitions in [L1] proves ν(E)<+. Applying this with E=X gives ν(X)<+.

L1L2L3step 2.1

Depends on

Used by

Dependency tree · two levels

12 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