LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-27

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.

A rational large-semicircle integral vanishes under the zR(z) to 0 condition

Statement

Let $R$ be a rational function, and for $T > 0$ let $γ_{T}^{+} (t) = T e^{i t}$ for $0 \leq t \leq π$ . Assume that $γ_{T}^{+}$ meets no pole of $R$ for all sufficiently large $T$ , and that

$\sup_{0 \leq t \leq π} ∣ γ_{T}^{+} (t) R (γ_{T}^{+} (t)) ∣ ⟶ 0 (T \to \infty) .$

Then

$\int_{γ_{T}^{+}} R (z) d z ⟶ 0 (T \to \infty) .$

Facts & Assumptions

Given: A rational function $R$ and the upper semicircles $γ_{T}^{+} (t) = T e^{i t}$ .

Proof

technique · direct

1.1given

Along $γ_{T}^{+}$ one has $∣ γ_{T}^{+} (t) ∣ = T$ , so $∣ R (γ_{T}^{+} (t)) ∣ \leq \frac{1}{T} \sup_{0 \leq s \leq π} ∣ γ_{T}^{+} (s) R (γ_{T}^{+} (s)) ∣ .$

2.1step 1.1

The arc length of $γ_{T}^{+}$ is $π T$ . Therefore the ML estimate gives $∣ \int_{γ_{T}^{+}} R (z) d z ∣ \leq π T \cdot \frac{1}{T} \sup_{0 \leq s \leq π} ∣ γ_{T}^{+} (s) R (γ_{T}^{+} (s)) ∣ = π \sup_{0 \leq s \leq π} ∣ γ_{T}^{+} (s) R (γ_{T}^{+} (s)) ∣ .$

3.1step 2.1∎

The right-hand side tends to $0$ by hypothesis, so the arc integral tends to $0$ as claimed.

Depends on

Standard semicircle, rectangle, keyhole, indentation, and sector contours

Used by

Dependency tree · two levels

4 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

L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 §5.3 (standard reference, not scraped)