LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

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 is positive, has total mass one, and concentrates at a boundary point

Statement

For $0 \leq r < 1$ , the Poisson kernel

$P_{r} (θ) = \frac{1 - r^{2}}{1 - 2 r \cos θ + r^{2}}$

has the following properties:

$P_{r} (θ) > 0$ for every $θ$ ;
$\frac{1}{2 π} \int_{0}^{2 π} P_{r} (θ) d θ = 1$ ;
for every $δ \in (0, π]$ , $\sup_{δ \leq ∣ θ ∣ \leq π} P_{r} (θ) ⟶ 0 (r \to 1^{-}) .$

Facts & Assumptions

Given: A radius $0 \leq r < 1$ .

[L1]

The Poisson kernel is the real part of the Möbius function $\frac{1 + r e^{i θ}}{1 - r e^{i θ}},$ because multiplying numerator and denominator by $1 - r e^{- i θ}$ gives the displayed quotient with real part $(1 - r^{2}) / (1 - 2 r \cos θ + r^{2})$ (The Poisson kernel on the unit disc, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[L2]

The function $w \mapsto \frac{1 + r w}{1 - r w}$ is holomorphic on the unit disc (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero) and equals its average on every unit circle by the holomorphic mean-value property (A holomorphic function equals its average on every circle inside a larger concentric holomorphy disc).

Proof

technique · direct

1.1

Since $1 - r^{2} > 0$ and $1 - 2 r \cos θ + r^{2} = (1 - r)^{2} + 2 r (1 - \cos θ) > 0,$ the quotient $P_{r} (θ)$ is positive for every $θ$ .

givenalgebra

1.2

By [L2], $1 = \frac{1}{2 π} \int_{0}^{2 π} \frac{1 + r e^{i θ}}{1 - r e^{i θ}} d θ .$ Taking real parts and using [L1] gives $\frac{1}{2 π} \int_{0}^{2 π} P_{r} (θ) d θ = 1$ .

L1L2

2.1

If $δ \leq ∣ θ ∣ \leq π$ , then $\cos θ \leq \cos δ$ , so $0 < P_{r} (θ) \leq \frac{1 - r^{2}}{1 - 2 r \cos δ + r^{2}} .$ The denominator tends to $2 (1 - \cos δ) > 0$ as $r \to 1^{-}$ , while the numerator tends to $0$ , so the right-hand side tends to $0$ , proving the uniform concentration estimate on representatives in $[- π, π]$ . Periodicity gives the equivalent formulation using circular distance from $0$ .

step 1.1algebra∎

Depends on

Used by

Dependency tree · two levels

16 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

Jeremy Orloff, MIT 18.04 Topic 5: Introduction to Harmonic Functions (standard reference, not scraped)
Sigurdur Helgason, MIT 18.112 Lecture 16: Harmonic Functions (standard reference, not scraped)