ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-10-02

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.

Infinity-pole Green function recovered from a circular conductor

Statement

Assume the Axiom of Choice. Let $a \in C$ , $r > 0$ , let $K : = \overline{D (a, r)}$ be the closed disc, and let $Ω : = {z \in C : ∣ z - a ∣ > r}$ be its exterior. Then the normalized infinity-pole Green function of $Ω$ is

$g_{Ω} (z, \infty) = g (z) : = \log \frac{∣ z - a ∣}{r} (z \in Ω),$

so that $g_{Ω} (z, \infty) = V_{K} - U^{μ_{K}} (z)$ on $Ω$ . Moreover $g$ has boundary limit $0$ at every point of the boundary circle ${z : ∣ z - a ∣ = r}$ , with no exceptional set, and $g (z) - \log ∣ z ∣ \to - \log r$ as $∣ z ∣ \to \infty$ .

The Axiom of Choice is spent through the equilibrium-measure input (Capacity of a disc and its circular equilibrium measure and Green function at infinity from the equilibrium potential); the explicit radial computations for $g$ are choice-free.

Facts & Assumptions

Given: $a \in C$ , $r > 0$ , the closed disc $K : = \overline{D (a, r)}$ , its exterior $Ω : = {z : ∣ z - a ∣ > r}$ , the Axiom of Choice, and the conventions of Logarithmic potential and energy of a positive compactly supported measure, Robin constant and logarithmic capacity of a compact set, Capacity-polar sets, quasi-everywhere, and subharmonic polar sets and Green function with a pole at infinity.

[F1]

Assume the Axiom of Choice. With $K : = \overline{D (a, r)}$ and $μ$ the normalized arclength measure $d μ = d t / (2 π)$ on the circle $w = a + r e^{i t}$ , $μ$ is the unique equilibrium measure of $K$ , $U^{μ} (z) = \log \frac{1}{r} (∣ z - a ∣ \leq r), U^{μ} (z) = \log \frac{1}{∣ z - a ∣} (∣ z - a ∣ \geq r),$ and $cap (K) = r$ with Robin constant $V_{K} = \log (1 / r)$ ; the same potential, capacity and equilibrium measure hold for the boundary circle (Capacity of a disc and its circular equilibrium measure).

[F2]

A Green function of $Ω$ with pole at infinity and Robin constant $V_{K}$ is a function $g : Ω \to R$ that is positive and harmonic on $Ω$ , satisfies $g (z) - \log ∣ z ∣ \to V_{K}$ as $∣ z ∣ \to \infty$ , is locally bounded near every point of $\partial Ω$ , and has boundary limit $0$ outside a Borel capacity-polar subset of $\partial Ω$ ; if existence and uniqueness hold the function is written $g_{Ω} (\cdot, \infty)$ (Green function with a pole at infinity).

[F3]

A compact set $K$ with $cap (K) > 0$ is nonempty, $Ω : = Ω (K)$ denotes the unbounded connected component of $C ∖ K$ and is a complex domain with compact boundary $\partial Ω \subseteq K$ , and $V_{K} = \inf_{μ \in P (K)} I (μ)$ is a real number (Green function with a pole at infinity, Robin constant and logarithmic capacity of a compact set).

[F4]

Assume the Axiom of Choice. For $K \subseteq C$ compact with $cap (K) > 0$ , the unbounded component $Ω$ of $C ∖ K$ , the equilibrium measure $μ_{K}$ and $V_{K} = \log \frac{1}{cap (K)}$ , the function $g (z) = V_{K} - U^{μ_{K}} (z)$ satisfies properties 1-4 of [F2], every function satisfying properties 1-4 equals it, and $g_{Ω} (z, \infty) = V_{K} - U^{μ_{K}} (z)$ on $Ω$ ; hence $K$ has exactly one Green function with pole at infinity (Green function at infinity from the equilibrium potential).

[F5]

For every $a \in C$ the function $u_{a} (z) = \log ∣ z - a ∣$ is smooth and harmonic on $C ∖ {a}$ ; no choice principle is required (Logarithmic modulus is harmonic off its centre, Plane harmonic functions).

[F6]

If $K \subseteq C$ is compact, the complement $C ∖ K$ has exactly one unbounded connected component and every other component is bounded; for $K = \overline{D (a, r)}$ that component is ${z : ∣ z - a ∣ > r}$ , which is therefore a complex domain (The complement of a compact plane set has exactly one unbounded connected component, A complex domain is a nonempty connected open subset of $C$ ).

[F7]

A set is capacity-polar when every compact subset of it has capacity zero; $\emptyset$ is capacity-polar, and a subset of a capacity-polar set is capacity-polar (Capacity-polar sets, quasi-everywhere, and subharmonic polar sets).

[F8]

The Axiom of Choice implies Dependent Choice, which implies Countable Choice (AC implies DC implies countable choice).

Verification

technique · direct

1.1F1F3F6given

Setup. With $K = \overline{D (a, r)}$ and $Ω = {z : ∣ z - a ∣ > r}$ , [F6] identifies $Ω$ with the unbounded connected component of $C ∖ K$ and makes it a complex domain with $\partial Ω = {z : ∣ z - a ∣ = r}$ ; by [F1] $cap (K) = r > 0$ , $V_{K} = \log \frac{1}{r}$ , and the equilibrium measure $μ_{K}$ has potential $U^{μ_{K}} (z) = \log \frac{1}{∣ z - a ∣}$ for $∣ z - a ∣ \geq r$ and $U^{μ_{K}} (z) = \log \frac{1}{r}$ for $∣ z - a ∣ \leq r$ .

1.2F5algebragiven

Positivity and harmonicity. Define $g (z) : = \log \frac{∣ z - a ∣}{r}$ for $z \in Ω$ . Then $g (z) > 0$ on $Ω$ , since $∣ z - a ∣ > r$ ; and $g$ is harmonic on $Ω$ , because $\log ∣ z - a ∣$ is harmonic on the open set $C ∖ {a} \supseteq Ω$ by [F5] and subtracting the constant $\log r$ leaves its Laplacian zero.

1.3givenalgebra

Boundary values, local boundedness and the infinity normalization. If $ξ \in \partial Ω$ , that is $∣ ξ - a ∣ = r$ , then for $z \in Ω$ , $∣ g (z) - 0 ∣ = \log \frac{∣ z - a ∣}{r} \to \log \frac{r}{r} = 0$ as $z \to ξ$ , and for every $δ > 0$ one has $\sup {g (z) : z \in Ω, ∣ z - ξ ∣ < δ} \leq \log \frac{r + δ}{r} < + \infty$ ; moreover $g (z) - \log ∣ z ∣ = \log \frac{∣ z - a ∣}{∣ z ∣} - \log r \to - \log r$ as $∣ z ∣ \to \infty$ , because $\frac{∣ z - a ∣}{∣ z ∣} \to 1$ and $\log$ is continuous at $1$ .

2.1step 1.1step 1.2F1

Identification with the equilibrium potential. On $Ω$ one has $∣ z - a ∣ > r$ , so by [F1] $U^{μ_{K}} (z) = \log \frac{1}{∣ z - a ∣}$ there and $V_{K} - U^{μ_{K}} (z) = \log \frac{1}{r} - \log \frac{1}{∣ z - a ∣} = \log \frac{∣ z - a ∣}{r} = g (z) .$

2.2step 1.2step 1.3F2F7

The explicit function is a Green function. Steps 1.2 and 1.3 give properties 1, 2 and 3 of [F2] for $g$ with Robin constant $V_{K} = \log \frac{1}{r}$ ; property 4 holds with the exceptional set $E : = \emptyset$ , because step 1.3 gives the boundary limit $0$ at every point of $\partial Ω$ , and $\emptyset$ is Borel and capacity-polar by [F7]. Hence $g$ is a Green function of $Ω$ with pole at infinity and Robin constant $V_{K}$ in the sense of [F2].

3.1step 1.1step 2.1step 2.2F4

Uniqueness and the notation. By step 1.1, $K$ is compact with $cap (K) = r > 0$ , so [F4] applies and gives: the Green function of $Ω$ with pole at infinity exists, every function satisfying properties 1-4 of [F2] equals $V_{K} - U^{μ_{K}}$ , and the notation $g_{Ω} (\cdot, \infty)$ is licensed with $g_{Ω} (z, \infty) = V_{K} - U^{μ_{K}} (z)$ on $Ω$ . By step 2.2 the function $g$ satisfies properties 1-4, so $g = V_{K} - U^{μ_{K}} = g_{Ω} (\cdot, \infty)$ on $Ω$ by step 2.1, and the boundary and normalization assertions are step 1.3.

4.1step 2.1step 3.1F1F4F8∎

Assembly and choice. Assertions of the Statement are exactly steps 2.1 and 3.1 (identification, notation, boundary limit on the entire circle and the infinity normalization); the boundary set is empty, so no exceptional set is needed. The Axiom of Choice is used only through [F1] and [F4], which by [F8] also supply Dependent and Countable Choice to their equilibrium-measure and Frostman inputs; the radial computations of steps 1.2, 1.3 and 2.1 are choice-free.

Remarks

Direct radial computation, not the general quasi-everywhere machinery. The properties of $g$ are verified here by direct radial computation: positivity and harmonicity came from $\log ∣ z - a ∣$ being harmonic off its centre, the boundary limit $0$ holds at every boundary point because $g = \log (∣ z - a ∣ / r)$ extends continuously to the closed exterior with value $0$ on the circle, and the normalization at infinity is the elementary limit $\log (∣ z - a ∣ / ∣ z ∣) \to 0$ . In particular the exceptional set in property 4 of Green function with a pole at infinity may be taken empty here; the general quasi-everywhere uniqueness theorem (Green function at infinity from the equilibrium potential) is invoked only for the uniqueness clause, where the ordinary maximum principle on the exterior alone would not suffice for candidates whose boundary limit is assumed only quasi-everywhere.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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

E. B. Saff, Logarithmic Potential Theory with Applications to Approximation Theory, §§1–3 (standard reference, not scraped)
B. Khoruzhenko, LTCC Potential Theory notes, §§3 and 5 (standard reference, not scraped)