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.
Uniqueness of a law from its characteristic function
Statement
Assume AC. Two Borel probability laws on with equal characteristic functions are equal. In particular a real random variable has a real-valued characteristic function if and only if its law is symmetric under .
Facts & Assumptions
Given: The hypotheses and conventions in the statement.
For a Borel probability law , the characteristic function is (Characteristic function of a real random variable). The finite-measure Fourier convention is (Fourier transform of a finite complex Borel measure). These bounded integrands are integrable; the latter theorem's countable-choice premise is covered by the stated AC.
Under AC finite complex Borel measures with equal transforms are equal. Uniqueness of finite Borel measures from their Fourier transforms.
AC supplies the choices in the Fourier uniqueness proof. The Axiom of Choice.
Reflection conjugates a characteristic function. Basic properties of characteristic functions.
The reflected law has characteristic function phi(-t). Characteristic functions under affine maps and independent sums.
Proof
Let be the two laws. Each positive probability law, regarded as a complex measure, has total variation one: every measurable partition has sum of absolute masses equal to its total mass. Thus [F1] applies in dimension one under the stated AC. For every real and , , so the defining bounded integrands are identical. Integrating this pointwise identity against either law gives and . Since the characteristic functions agree at every real argument, for every . This also verifies the finite-variation hypotheses of Fourier uniqueness.
Apply F2 in dimension one to obtain . AC is inherited from that proof: it supplies the Hahn/Jordan and Radon–Nikodym selections used in Gaussian smoothing and covers its regularity argument. No inversion result from this page is used.
For the final equivalence, F5 with and F4 give . If is real-valued, the two characteristic functions agree and step 2.1 proves symmetry of the law. Conversely, symmetry means the two laws, hence their defining integrals, agree; the displayed identity then forces , so every value is real.