Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

Distributions supported at one point

Statement

For aΩ and uD(Ω), suppu{a} if and only if u=αmcααδa for some finite m0 and complex coefficients. The coefficients, with absent higher terms interpreted as zero, are unique. A nonzero such combination has support exactly {a}; the zero combination has empty support. This holds in ZF.

Facts & Assumptions

[F1]

Dirac derivatives evaluate tests by αδa(φ)=(1)ααφ(a) (Dirac delta and its derivatives).

[F2]

Compact support gives one finite-order estimate on a compact neighborhood for every test (Compactly supported distributions have global finite order). Two tests that agree on a neighborhood of the distributional support have equal pairings, and empty support is equivalent to the zero distribution (Support of a distribution).

[F3]

Smooth compact cutoffs equal to one near a prescribed compact set exist in ZF (Test function cutoffs and euclidean localization).

[F4]

On an open convex neighborhood, the Taylor remainder for a Ck function is o(hk) for k1 (Multivariable Taylor formula with o(hk) remainder). Apply separately to real and imaginary parts; for degree zero use continuity directly.

Proof

Given: aΩ and a distribution u.

1.1

Suppose its support is contained in {a}. Obtain an order m and constant from F2. Take a fixed smooth χ equal to one near zero with support in a ball B(0,R), using F3 in Euclidean space. For all sufficiently small ε>0, χε(x)=χ((xa)/ε) is supported inside Ω and equals one near a. Hence u(φ)=u(χεφ) for every test.

givenF2F3
2.1

Suppose γφ(a)=0 for every γm. For fixed γ, Taylor's formula F4 on a ball about a applied to γφ gives γφ(a+h)=o(hmγ); when γ=m this is continuity with value zero. The little-o bounds are uniform over hRε by their definition: their suprema are o(εmγ). The product rule expands a derivative of order β, βm, of χεφ into finitely many terms [step 1.1, F2, F4, algebra] (βγ)εβγ(βγχ)((xa)/ε)γφ(x),γβ. Each has supremum o(εmβ), hence tends to zero, even when β=m. All derivatives vanish outside the shrinking support. Thus F2 and step 1.1 give u(φ)Cmaxβmsupβ(χεφ)0, so u(φ)=0.

step 1.1F2F4algebra
3.1

Take a fixed cutoff η equal to one near a and compactly supported in Ω. For αm put qα(x)=η(x)(xa)α/α!. Direct monomial differentiation gives βqα(a)=1 for β=α and zero for every other βm. Therefore φαmαφ(a)qα has zero jet through degree m. Step 2.1 makes its pairing zero, giving u(φ)=u(qα)αφ(a). By F1 this is the claimed representation with cα=(1)αu(qα).

step 2.1F1F3
4.1

Conversely, every test supported in Ω{a} has all derivatives zero at a, so F1 makes every displayed combination vanish there. Its support is therefore contained in {a}. Evaluate a zero combination on the tests qα constructed with the largest order occurring to see each coefficient is zero. This proves uniqueness. Finally a nonzero distribution cannot have empty support by locality (as used in F2), so a nonzero combination has support exactly {a}. The zero combination is allowed with m=0,c0=0. All jets and sums are finite and no choice is used.

step 3.1F1F2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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