ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 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.

The signed measure delta_1 minus delta_-1 has the obvious Hahn and Jordan decomposition

Example

On $(R, B (R))$ , let $ν : = δ_{1} - δ_{- 1} .$ Then $P = R ∖ {- 1}$ is positive, $N = {- 1}$ is negative, and $ν^{+} = δ_{1}, ν^{-} = δ_{- 1}, ∣ ν ∣ = δ_{1} + δ_{- 1} .$

Facts & Assumptions

Given: The Dirac set functions $δ_{1}$ and $δ_{- 1}$ .

[L1]

The Dirac set function at a point is the indicator-valued set function on measurable sets. (The Dirac set function at a point)

[L2]

Hahn decomposition splits a signed measure into a positive part and a negative part, and Jordan decomposition records the corresponding measures. (Hahn decomposition for signed measures, unique up to total-variation-null sets, Jordan decomposition of a signed measure into unique mutually singular positive parts)

Verification

technique · direct

1.1

By [L1], for every measurable $E$ one has [L1, L2] $ν (E) = 1_{E} (1) - 1_{E} (- 1)$ . If $E \subseteq P$ is measurable, then $- 1 \notin E$ , so $ν (E) = 1_{E} (1) \geq 0$ . If $E \subseteq N$ is measurable, then $1 \notin E$ , so $ν (E) = - 1_{E} (- 1) \leq 0$ . Thus $P$ is positive and $N$ is negative.

L1L2

2.1

Since $R = P ⊔ N$ , step 1.1 gives a Hahn decomposition. [L2, step 1.1] The Jordan measures are therefore $δ_{1}$ and $δ_{- 1}$ , so $∣ ν ∣ = δ_{1} + δ_{- 1}$ by [L2]. ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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

John K. Hunter, Measure Theory, Example 6.14 (standard reference, not scraped)