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.
Compactly supported smooth functions are unique from any open set of Radon angles
Statement
Let be a nonempty open set of unit line normals and let . If the line integral is zero for every and , then is zero everywhere. The assertion holds without Countable Choice.
Statement references
Facts & Assumptions
Given: A nonempty open set , a compactly supported smooth complex function , and the hypothesis for every measured normal and offset.
For this proof, put . Since is nonempty and open, it contains an open arc , and the positive-radius sector is a nonempty open subset of .
The Fourier-slice identity for the Euclidean Radon transform: for compactly supported smooth input and the line-normal convention, for all real ; the supplier proof uses no Countable Choice.
The compact-support Fourier-Laplace transform is entire in each coordinate: the compact-support Riemann Fourier-Laplace transform of a smooth compactly supported function is entire in each coordinate, with coordinate derivatives given by integrals with polynomial factors; the proof is choice-free.
Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in : the real Riemann integral is linear, monotone, and bounded by volume times a uniform absolute bound; apply it componentwise to complex functions.
Identity theorem for holomorphic functions: a holomorphic function on a connected domain that vanishes on a set with an accumulation point in the domain vanishes everywhere.
Real Stone--Weierstrass theorem for compact metric spaces: real polynomials on a compact subset of are dense in its real continuous functions because they form a unital point-separating algebra.
Proof
The hypothesis and the compact-support Fourier-slice identity [F2] give for every and . By [F1], this includes the nonempty open positive-radius sector generated by ; choose a product of open real intervals inside that sector. For each real , the entire function vanishes on , so [F5] makes it zero for every complex . Then for every real the entire second-coordinate slice vanishes on , and [F5] makes it zero everywhere. Thus vanishes on all of .
Let . If , then . Otherwise, fix a rectangle whose interior contains and interpret all integrals below as compact-support Riemann integrals over . Repeated use of the coordinate derivative formula in [F3] shows for every multi-index , since all real-frequency derivatives of vanish at the origin. The real polynomials restricted to form a unital subalgebra separating points, because the coordinate functions distinguish distinct points. For an arbitrary , apply [F6] separately to and with error and combine the two real polynomials into one complex polynomial with . Every moment is zero, so . Since outside , the real Riemann integral bound [F4] on both components gives . As this holds for every , ; no sequence of approximants is selected. If were nonzero at a point, continuity would bound below by a positive number on a nondegenerate box inside , forcing its nonnegative Riemann integral to be positive. Thus everywhere. This proof uses neither Fourier inversion nor Countable Choice.
Depends on
- The Fourier-slice identity for the Euclidean Radon transform
- The compact-support Fourier-Laplace transform is entire in each coordinate
- Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $\mathbb{R}^m$
- Identity theorem for holomorphic functions
- Real Stone--Weierstrass theorem for compact metric spaces
Used by
Dependency tree · two levels
34 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
- Mikko Salo, On geometric inverse problems and microlocal analysis, §2.1 (standard reference, not scraped)
- Venkataswaran P. Krishnan and Eric Todd Quinto, Microlocal Analysis in Tomography (standard reference, not scraped)