Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05
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 Poisson kernel on the circle is a positive approximate identity

Statement

For 0r<1, let

Pr(t):=kZrkek(t).

Then

Pr(t)=1r212rcos(2πt)+r2.

Hence Pr(t)0 for every t, 01Pr(t)dt=1, and for every δ(0,1/2],

supt[δ,1δ]Pr(t)0(r1).

In particular,

δ1δPr(t)dt0(r1).

Facts & Assumptions

Given: A parameter r with 0r<1 and a real δ(0,1/2].

[L1]

The Poisson kernel Pr and the characters ek(t)=e2πikt are defined in Cesaro and Abel means of a Fourier series and Period-one Fourier coefficients, partial sums, and convolution on the torus.

Proof

technique · direct
1.1

Let z=e2πit. By [L1], Pr(t)=1+k=1rkzk+k=1rkzk. Both geometric series converge absolutely, so Pr(t)=1+rz1rz+rz11rz1=1r2(1rz)(1rz1). Since z+z1=2cos(2πt), this is exactly Pr(t)=1r212rcos(2πt)+r2.

L1algebra
2.1

Step 1.1 shows Pr(t)0 because 12rcos(2πt)+r2=(1r)2+2r(1cos(2πt))0, and the numerator is positive for r<1. Also the constant Fourier coefficient of Pr is 1, so 01Pr(t)dt=1.

L1step 1.1algebra
3.1

The limit only concerns r1, so it is enough to consider r[1/2,1). If t[δ,1δ], then 12rcos(2πt)+r2=(1r)2+4rsin2(πt)2sin2(πδ). Therefore step 1.1 gives Pr(t)1r22sin2(πδ). As r1, the right-hand side tends to 0, so the displayed supremum tends to 0. Multiplying that supremum bound by the interval length at most 1 gives the same limit for the tail integral.

step 1.1algebra

Depends on

Used by

Dependency tree · two levels

3 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