ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

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.

Harmonic measure of a real interval from the upper half-plane

Example

Assume the Axiom of Countable Choice for the explicit Borel measure interface. Let $a < b$ be real, let $H = {z : Im z > 0}$ , and let $ω_{H}^{z}$ be the upper half-plane harmonic measure of The upper half-plane Poisson boundary density, so that $d ω_{H}^{z} (t) = k_{z} (t) d t$ with $k_{z} (t) = y / (π ((t - x)^{2} + y^{2}))$ for $z = x + i y$ . Then for every $z \in H$ $ω_{H}^{z} ([a, b]) = \frac{1}{π} (\arctan \frac{b - x}{y} - \arctan \frac{a - x}{y}),$ a number in $[0, 1]$ . The value tends to $1$ as $z$ approaches an interior point of $[a, b]$ , to $0$ as $z$ approaches a point outside $[a, b]$ , and to $1 / 2$ at an endpoint approached vertically along the perpendicular. The arctangent calculation itself is choice-free; ${A C}_{ω}$ enters through the inherited Borel-measure and Lebesgue-integral interface, including the Riemann-to-Lebesgue comparison.

Facts & Assumptions

Given: Real numbers $a < b$ , a point $z = x + i y \in H$ with $y > 0$ , and the Axiom of Countable Choice for the Lebesgue interface (The Axiom of Countable Choice ( ${A C}_{ω}$ )). The closed interval $[a, b]$ is a Borel subset of $R$ (The Borel sigma-algebra of a topological space), and $ω_{H}^{z}$ is the Borel probability measure of The upper half-plane Poisson boundary density with density $k_{z}$ there.

[F1]

For $z \in H$ the density $k_{z} (t) = y / (π ((t - x)^{2} + y^{2}))$ is continuous and nonnegative, $ω_{H}^{z} (A) = \int_{A} k_{z} d λ_{1}$ is a Borel probability measure, and $ω_{H}^{z}$ was obtained under ${A C}_{ω}$ (The upper half-plane Poisson boundary density).

[F2]

The principal inverse tangent is strictly increasing with $\frac{d}{d x} \arctan x = 1 / (1 + x^{2})$ , $\arctan x = \int_{0}^{x} d t / (1 + t^{2})$ and $\arctan s \to \pm π / 2$ as $s \to \pm \infty$ (The principal inverse tangent $\arctan : R \to (- π / 2, π / 2)$ , Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series).

[F3]

One-dimensional change of variables: for $C^{1}$ injective $φ$ with $φ^{'} \neq 0$ near $[a, b]$ and continuous $g$ on an interval containing $φ ([a, b])$ , $\int_{\min φ}^{\max φ} g (s) d s = \int_{a}^{b} g (φ (t)) ∣ φ^{'} (t) ∣ d t$ (In one dimension the compact-Jordan formula is substitution over the unoriented image interval with the absolute derivative); a continuous function on a compact interval is Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion); and a bounded Riemann integrable function on a compact interval is Lebesgue measurable with the same integral (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral).

Verification

technique · direct

1.1F1F3given

The density $k_{z}$ is continuous and nonnegative on $R$ by [F1], so its restriction to the compact interval $[a, b]$ is Riemann integrable by [F3]; the interval is Borel, so the integral $\int_{[a, b]} k_{z} d λ_{1}$ defining $ω_{H}^{z} ([a, b])$ is well posed.

2.1F2F3step 1.1algebra

Substituting $s = (t - x) / y$ on $[a, b]$ , admissible by [F3] with $φ (t) = (t - x) / y$ (so $φ^{'} = 1 / y \neq 0$ ) and $g (s) = 1 / (π (1 + s^{2}))$ , gives for the Riemann integral $\int_{a}^{b} k_{z} (t) d t = \frac{1}{π} \int_{(a - x) / y}^{(b - x) / y} \frac{d s}{1 + s^{2}} = \frac{1}{π} (\arctan \frac{b - x}{y} - \arctan \frac{a - x}{y}),$ the last equality by the antiderivative in [F2].

3.1F1F3step 2.1

By the Riemann-Lebesgue agreement of [F3] the same value is the Lebesgue integral of $k_{z}$ over $[a, b]$ , hence $ω_{H}^{z} ([a, b]) = \frac{1}{π} (\arctan \frac{b - x}{y} - \arctan \frac{a - x}{y}) .$

4.1F2step 3.1algebra

The displayed value lies in $[0, 1]$ : it is nonnegative because $\arctan$ is strictly increasing and $a < b$ imply $\arctan ((a - x) / y) < \arctan ((b - x) / y)$ , and it is at most $(π / 2 - (- π / 2)) / π = 1$ because $\arctan$ takes values in $(- π / 2, π / 2)$ .

4.2F2step 3.1cases

Boundary values. If $t_{0} \in (a, b)$ and $z \to t_{0}$ with $z \in H$ , then $(b - x) / y \to + \infty$ and $(a - x) / y \to - \infty$ , so the value tends to $(π / 2 + π / 2) / π = 1$ . If $t_{0} \notin [a, b]$ , then $(b - x) / y$ and $(a - x) / y$ tend to the same signed infinity, so their arctangents have the same limit and the value tends to $0$ . If $t_{0} = a$ and $z$ approaches $a$ with $x = a$ , then $(a - x) / y = 0$ and $(b - x) / y \to + \infty$ , so the value tends to $(π / 2 - 0) / π = 1 / 2$ ; the same computation at $t_{0} = b$ gives $1 / 2$ .

5.1F1F3step 3.1step 4.1step 4.2∎

Therefore the harmonic measure of a real interval for the upper half-plane is the explicit arctangent expression of step 3.1, bounded between zero and one by step 4.1 and attaining the boundary values one, zero and one half in the three configurations of step 4.2. The use of ${A C}_{ω}$ is inherited through the Borel-measure and Lebesgue-integral interface in steps 1.1 and 3.1, including their Riemann-to-Lebesgue comparison.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

84 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

Boris Khoruzhenko, LTCC Potential Theory lecture notes, Sections 4.1-4.2 (standard reference, not scraped)