Alphabeta Math
LemmaStatement: 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 set of positive finite signed measure contains a positive subset of at least the same mass

Statement

Assume the Axiom of Choice. Let ν be a signed measure on (X,A) and let A∈A satisfy 0<ν(A)<+∞. Then there exists a positive set P⊆A such that ν(P)≥ν(A).

Facts & Assumptions

Given: A signed measure ν, a measurable set A with 0<ν(A)<+∞, and the Axiom of Choice (The Axiom of Choice).

[L1]

A measurable set is positive when every measurable subset has nonnegative signed measure. (Positive, negative, and null sets for a signed measure)

[L2]

Every measurable subset of A has finite signed measure. (A subset of a set of finite signed measure also has finite signed measure)

[L3]

If a disjoint union has finite signed measure, then the resulting real series converges absolutely. (If a disjoint union has finite signed measure, then the signed-measure series converges absolutely)

Proof

technique · direct
1.1givenL1L2choose

For each n≥1 and measurable R⊆A, put δ(R)=inf⁡{ν(E):E∈A, E⊆R}. If R is positive, prescribe the subset ∅. Otherwise δ(R)<0: if it is finite, the subsets E⊆R with ν(E)≤δ(R)/2 form a nonempty family; if it is −∞, use the nonempty family with ν(E)≤−n. Apply AC to this set-indexed family of nonempty admissible-subset families to fix a selector E(n,R). Define recursively R1=A, An=E(n,Rn), δn=δ(Rn) and Rn+1=Rn∖An. The An are pairwise disjoint, have finite nonpositive values by [L2], and satisfy δn≤ν(An)≤δn/2 when δn is finite, and ν(An)≤−n otherwise. This selector is the precise use of AC; no minimal choice principle is asserted.

2.1L2L3step 1.1

Put B:=⋃n≥1An and P:=A∖B. Because B⊆A, [L2] makes ν(B) finite, and [L3] makes ∑n≥1ν(An) absolutely convergent. Thus ν(An)→0, and only finitely many terms satisfy ν(An)≤−1. The δn=−∞ branch therefore occurs only finitely often. For some n0 and every n≥n0, δn is finite and 0≥δn≥2ν(An). Comparison proves convergence of the tail ∑n≥n0∣δn∣, and in particular δn→0. No assertion about summing earlier infinite values is needed.

3.1L1step 1.1step 2.1

If E⊆P is measurable, then E⊆Rn for every n, so ν(E)≥δn by definition of δn. Letting n→∞ in step 2.1 gives ν(E)≥0, so [L1] shows that P is positive.

3.2step 2.1algebra

Because every term ν(An) is nonpositive, step 2.1 gives ν(B)=∑n≥1ν(An)≤0. Hence ν(P)=ν(A)−ν(B)≥ν(A).

4.1step 3.1step 3.2∎

Steps 3.1 and 3.2 give a positive subset P⊆A with ν(P)≥ν(A).

Depends on

Used by

Dependency tree · two levels

8 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