Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass
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.

Fourier transform of the three-dimensional plane Poisson kernel

Statement

For t>0 and z∈R2, let Pt(z)=t2π(∣z∣2+t2)3/2. Then Pt∈L1(R2) has integral one and, under the negative-sign 2π Fourier convention, Pt^(ξ)=e−2π∣ξ∣t(ξ∈R2).

Facts & Assumptions

Given: Countable Choice (The Axiom of Countable Choice (ACω)), t>0, the displayed kernel, and the Fourier convention.

[A1]

Countable Choice is assumed for the Fourier and polar-measure constructions (The Axiom of Countable Choice (ACω)).

[F1]

The L1 Fourier transform is a bounded function, agrees with the distributional transform, and sends a second distributional derivative to multiplication by (2πiξj)2 (Fourier transform agrees with l one and plancherel transforms, Fourier differentiation and multiplication identities on tempered distributions).

[F2]

In dimension two the angular measure in [F90] has mass 2π: the parametrization (cos⁡θ,sin⁡θ), 0<θ<2π, has unit speed and covers the circle except one surface-null point. Thus ∫R2a(∣z∣)dz=2π∫0∞a(r)r dr for nonnegative radial a. The parametrization and one-variable integrations use the sine/cosine derivatives and FTC. (The derivatives of sine and cosine are cosine and minus sine, The second fundamental theorem: if G is differentiable on [a,b] with G′=f and f is integrable, then ∫abf=G(b)−G(a))

[F90]

Polar integration uses the published radial formula, not a linear substitution: dx=rn−1dr dσ(ω). The sphere measure agrees with graph-chart surface measure and scales by Rn−1. (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, Agreement with the existing polar sphere measure)

Proof

1.1F2F90givenalgebra

In polar coordinates, ∫R2Pt(z) dz=t∫0∞r(r2+t2)−3/2dr=1; the same estimate shows Pt∈L1. Direct differentiation of t(∣z∣2+t2)−3/2 gives (Δz+∂t2)Pt=0 for t>0.

2.1A1F1step 1.1givenalgebra∎

Put F(t,ξ)=Pt^(ξ). For t in any compact subinterval of (0,∞), Pt and its first two t-derivatives are dominated by integrable radial functions, so differentiation under the Fourier integral is valid. Fourier transforming the harmonic identity in step 1.1 and using [F1] gives ∂t2F−(2π∣ξ∣)2F=0. Also ∣F(t,ξ)∣≤∥Pt∥1=1. For fixed ξ, the change z=tw gives F(t,ξ)=∫R2P1(w)e−2πitw⋅ξdw; dominated convergence yields F(t,ξ)→1 as t↓0. The solutions of this constant-coefficient ODE are linear combinations of e2π∣ξ∣t and e−2π∣ξ∣t when ξ≠0; boundedness removes the growing term, and the boundary limit fixes the coefficient to one. When ξ=0, the bounded affine solutions are constant and the same limit gives one. Hence F(t,ξ)=e−2π∣ξ∣t.

Depends on

Used by

Dependency tree · two levels

77 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