Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Jordan's lemma for rational functions of one complex variable

Statement

Let λ>0, let R be a rational function, and let γT+(t)=Teit for 0≤t≤π. Assume that γT+ meets no pole of R for all sufficiently large T, and that

sup⁡0≤t≤π∣ γT+(t) R(γT+(t)) ∣⟶0(T→∞).

Then

∫γT+eiλzR(z) dz⟶0(T→∞).

Facts & Assumptions

Given: A real number λ>0, a rational function R, and the upper semicircles γT+(t)=Teit.

[L1]

If a twice differentiable function on an interval has nonnegative second derivative, then it is convex (A twice-differentiable function on an open interval is convex if and only if its second derivative is nonnegative).

Proof

technique · direct
1.1givenalgebra

For z=Teit on the upper semicircle, ∣eiλz∣=∣eiλT(cos⁡t+isin⁡t)∣=e−λTsin⁡t.

1.2L1

On [0,π/2] the function g(t)=−sin⁡t has [L1, algebra] g′′(t)=sin⁡t≥0, so makes g convex there. A convex graph lies below the chord joining its endpoint values, hence −sin⁡t≤−2t/π and therefore sin⁡t≥2tπ(0≤t≤π2). By symmetry, also sin⁡t≥2(π−t)π(π2≤t≤π).

2.1step 1.1given

Put MT:=sup⁡0≤t≤π∣ γT+(t)R(γT+(t)) ∣. Then along the arc ∣eiλzR(z) dz∣≤e−λTsin⁡tMTT T dt=MTe−λTsin⁡t dt. So ∣∫γT+eiλzR(z) dz∣≤MT∫0πe−λTsin⁡t dt.

3.1step 2.1step 1.2algebra

Splitting the integral at π/2 and using step 1.2 gives ∫0πe−λTsin⁡t dt≤2∫0π/2e−2λTt/π dt=πλT(1−e−λT)≤πλT. Hence ∣∫γT+eiλzR(z) dz∣≤πMTλT.

4.1step 3.1∎

Since MT→0, the bound in step 3.1 tends to 0. Therefore the arc integral tends to 0.

Depends on

Used by

Dependency tree · two levels

9 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