LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

The sine integral under Countable Choice: uniform bounds and the value pi/2

Statement

Assume Countable Choice. Put $f (u) : = \sin (u) / u$ for $u > 0$ and $f (0) : = 1$ , and write $S (T) : = \int_{0}^{T} f (u) d u$ for $T \geq 0$ . Then:

$S (T) \to π / 2$ as $T \to \infty$ ; that is, the improper integral $\int_{0}^{\infty} \sin (u) / u d u$ converges and equals $π / 2$ .
The partial integrals are uniformly bounded: $∣ S (T) ∣ \leq 3$ for every $T \geq 0$ , moreover $∣ S (T) ∣ \leq T$ for $0 \leq T \leq 1$ , and more precisely $∣ \int_{A}^{B} \sin (u) / u d u ∣ \leq 2 / A$ for all $1 \leq A < B$ .
For every real $z$ and every $T \geq 0$ , reading the integrand at $t = 0$ as $z$ ,

$\int_{- T}^{T} \frac{\sin (t z)}{t} d t = 2 sgn (z) S (T ∣ z ∣),$

so that $\lim_{T \to \infty} \int_{- T}^{T} \sin (t z) / t d t = π sgn (z)$ and $∣ \int_{- T}^{T} \sin (t z) / t d t ∣ \leq 6$ for every $T \geq 0$ and every real $z$ .

The argument uses Countable Choice only; it does not invoke the published full-AC sine-integral lemma of the same name on the Dirichlet-kernel page.

Facts & Assumptions

Given: Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) and the functions $f$ and $S$ of the statement.

[F1]

Integration by parts on a compact interval for differentiable factors with integrable derivatives. If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$

[F2]

The second fundamental theorem: an integrable derivative integrates to the endpoint increment. The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$

[F3]

Under Countable Choice a bounded Riemann integrable function on a compact interval is Lebesgue measurable, and its Riemann and Lebesgue integrals agree. A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral

[F4]

Fubini's theorem for L^1 functions on a sigma-finite product. Fubini's theorem for L^1 functions on a sigma-finite product

[F5]

Tonelli's theorem for nonnegative product-measurable functions on a sigma-finite product. Tonelli's theorem for nonnegative measurable functions on a sigma-finite product

[F6]

Dominated convergence. Dominated convergence

[F7]

Sine and cosine have derivatives cosine and minus sine, and $\sin 0 = 0$ , $\cos 0 = 1$ . The derivatives of sine and cosine are cosine and minus sine

[F8]

The real exponential is its own derivative. The exponential function is smooth and $(\exp)^{'} = \exp$

[F9]

The chain rule. The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$

[F10]

$1 + x \leq e^{x}$ for every real $x$ , hence $e^{- x} \leq 1 / (1 + x)$ for $x \geq 0$ and $e^{- x} \to 0$ as $x \to \infty$ . $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$

[F11]

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

[F12]

Sine and cosine are 1-Lipschitz: $∣ \sin u - \sin v ∣ \leq ∣ u - v ∣$ and $∣ \cos u - \cos v ∣ \leq ∣ u - v ∣$ . Sine and cosine are $1$ -Lipschitz on $R$

[F13]

Parity and the Pythagorean identity: $\sin (- x) = - \sin x$ , $\cos (- x) = \cos x$ , $\sin^{2} x + \cos^{2} x = 1$ , hence $∣ \sin x ∣ \leq 1$ and $∣ \cos x ∣ \leq 1$ . Parity and the Pythagorean identity for sine and cosine

[F14]

Continuous maps on Euclidean spaces are Borel measurable, so the product integrands below are measurable. Continuous functions on Euclidean spaces are Borel measurable

[F15]

Change of variable for improper integrals: for a monotone differentiable surjection satisfying the proper hypotheses on compact truncations, the two improper integrals converge simultaneously and are equal, with orientation retained for decreasing parametrizations. Change of variable in an improper integral

[F16]

Principal arctangent: $\arctan^{'} = 1 / (1 + x^{2})$ and $\arctan x = \int_{0}^{x} d t / (1 + t^{2})$ . Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series

[F17]

Principal arctangent is a continuous strictly increasing bijection from $R$ onto $(- π / 2, π / 2)$ , and $\arctan (\tan x) = x$ on the principal interval. The principal inverse tangent $\arctan : R \to (- π / 2, π / 2)$

[F18]

A convergent nonnegative improper Riemann integral on a half-line agrees with the Lebesgue integral of its integrand, under Countable Choice. A nonnegative improper Riemann integral on a half-line agrees with the Lebesgue integral

[F19]

Additivity of the integral over subintervals, in the oriented form. For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$

Proof

technique · direct

1.1F7F12F13

By [F7], $\sin 0 = 0$ and $\sin^{'} (0) = \cos 0 = 1$ , so $\sin (u) / u \to 1 = f (0)$ as $u \to 0$ ; and [F12] with $v = 0$ gives $∣ \sin u ∣ \leq u$ for $u \geq 0$ , while [F13] gives $∣ \cos u ∣ \leq 1$ . Thus $f$ is bounded by $1$ on $[0, \infty)$ and continuous at $0$ from the right.

1.2F2F8F9F10F18

For $u \geq 0$ and $ε > 0$ , [F8] and [F9] give $(e^{- ε u})^{'} = - ε e^{- ε u}$ , and [F10] bounds $e^{- ε u} \leq 1 / (1 + ε u)$ , so $e^{- ε u} \to 0$ as $u \to \infty$ ; [F2] applied to $u \mapsto - e^{- ε u} / ε$ therefore gives $\int_{0}^{R} e^{- ε u} d u = (1 - e^{- ε R}) / ε$ for every $R > 0$ , and this tends to $1 / ε$ as $R \to \infty$ when $ε > 0$ . By [F18] the nonnegative continuous function $u \mapsto e^{- ε u}$ is Lebesgue integrable on $[0, \infty)$ with $\int_{[0, \infty)} e^{- ε u} d λ (u) = 1 / ε$ .

1.3F2F7F8F9F10F12F13

For $t > 0$ , [F2] applied to $s \mapsto \sin (s t) / t$ , whose derivative is $\cos (s t)$ by [F7] and [F9], gives $\int_{0}^{1} \cos (s t) d s = \sin (t) / t$ , and at $t = 0$ both sides equal $1$ . For $ε > 0$ and $s \in [0, 1]$ put $H (t) : = e^{- ε t} (- ε \cos (s t) + s \sin (s t)) / (ε^{2} + s^{2})$ ; [F8], [F9] and [F7] give $H^{'} (t) = e^{- ε t} \cos (s t)$ , while [F10], [F12] and [F13] give $H (0) = - ε / (ε^{2} + s^{2})$ and $H (t) \to 0$ as $t \to \infty$ .

2.1step 1.1F11

By 1.1 the quotient $u \mapsto \sin (u) / u$ is continuous on $(0, \infty)$ and extends continuously to $u = 0$ with value $1$ , and it is bounded by $1$ there; by [F11] it is Riemann integrable on every compact interval $[0, T]$ , $T > 0$ .

2.2step 1.1F1F2F7F8F9

Let $1 \leq A < B$ and $0 \leq ε \leq 1$ , and put $w (u) : = e^{- ε u} / u$ on $[A, B]$ . By [F8] and [F9], $w$ is continuously differentiable with $w^{'} (u) = - e^{- ε u} (ε u + 1) / u^{2} \leq 0$ , so $w$ is nonincreasing, $w^{'} > 0$ holds nowhere, and [F2] gives $\int_{A}^{B} ∣ w^{'} ∣ = w (A) - w (B)$ . Since $(\cos u)^{'} = - \sin u$ by [F7], [F1] applies with factors $w$ and $- \cos$ and, using $∣ \cos ∣ \leq 1$ from 1.1, yields $∣ \int_{A}^{B} w (u) \sin u d u ∣ \leq w (A) + w (B) + \int_{A}^{B} ∣ w^{'} ∣ = 2 w (A) \leq 2 / A$ ; at $ε = 0$ this is $∣ \int_{A}^{B} \sin (u) / u d u ∣ \leq 2 / A$ .

3.1givenstep 2.1step 2.2F3F11

Under the given Countable Choice, [F3] applies on every compact interval: for the continuous integrands $f$ , $e^{- ε t} f$ and $e^{- ε t} \cos (s t)$ of steps 2.1 and 2.2, the proper Riemann integral on $[0, T]$ or $[A, B]$ equals the corresponding Lebesgue integral.

3.2step 2.1step 2.2F19

By 2.1 and [F19], for $T \geq 1$ one has $S (T) = \int_{0}^{1} f + \int_{1}^{T} \sin (u) / u d u$ with $∣ \int_{0}^{1} f ∣ \leq 1$ and $∣ \int_{1}^{T} \sin (u) / u d u ∣ \leq 2$ by 2.2; for $0 \leq T \leq 1$ the bound $∣ S (T) ∣ \leq T$ follows from $∣ f ∣ \leq 1$ in 2.1, and $T \leq 1$ gives $∣ S (T) ∣ \leq 1$ . Hence $∣ S (T) ∣ \leq 3$ for every $T \geq 0$ and $∣ S (T) ∣ \leq T$ on $[0, 1]$ .

4.1step 1.2step 1.3step 3.1F6

Fix $s \in [0, 1]$ and $ε > 0$ . By [F6] applied on $[0, \infty)$ to the functions $t \mapsto e^{- ε t} \cos (s t) χ_{[0, T]} (t)$ as $T \to \infty$ , which converge pointwise to $t \mapsto e^{- ε t} \cos (s t)$ and are dominated by the integrable function $e^{- ε t}$ of 1.2, and by 3.1 and 1.3, $\int_{[0, \infty)} e^{- ε t} \cos (s t) d λ (t) = \lim_{T \to \infty} H (T) - H (0) = ε / (ε^{2} + s^{2})$ .

4.2step 1.2step 2.2step 3.1F6

Let $A \geq 1$ and $0 < ε \leq 1$ . The functions $t \mapsto e^{- ε t} f (t) χ_{[A, B]} (t)$ converge pointwise as $B \to \infty$ to $t \mapsto e^{- ε t} f (t) χ_{[A, \infty)} (t)$ and are dominated by the integrable function $e^{- ε t} χ_{[A, \infty)}$ , so [F6] with 2.2 and 3.1 gives $∣ \int_{[A, \infty)} e^{- ε t} f (t) d λ (t) ∣ = \lim_{B \to \infty} ∣ \int_{A}^{B} e^{- ε t} f (t) d t ∣ \leq 2 / A$ . For $ε = 0$ , the bound in 2.2 makes $\int_{A}^{B} f (t) d t$ Cauchy as $B \to \infty$ and bounds the resulting improper tail by $2 / A$ .

4.3step 2.1step 3.1F6

For fixed $A > 0$ , $e^{- ε t} f (t) \to f (t)$ as $ε ↓ 0$ for every $t \in [0, A]$ , with $∣ e^{- ε t} f (t) ∣ \leq 1$ and $[0, A]$ of finite measure, so [F6] and 3.1 give $\int_{[0, A]} e^{- ε t} f (t) d λ (t) \to \int_{[0, A]} f (t) d λ (t) = S (A)$ as $ε ↓ 0$ .

5.1step 1.2step 1.3step 3.1step 4.1F4F5F14F15F16

Fix $ε > 0$ and put $Φ (s, t) : = e^{- ε t} \cos (s t)$ on $[0, 1] \times [0, \infty)$ . By [F14] the integrand $Φ$ is product measurable, and [F5] with 1.2 gives $\int_{[0, 1] \times [0, \infty)} ∣ Φ ∣ d (λ \otimes λ) \leq \int_{[0, 1]} (\int_{[0, \infty)} e^{- ε t} d λ (t)) d s = 1 / ε < \infty$ , so $Φ \in L^{1}$ of the product and [F4] may be applied. By 1.3, 3.1 and 4.1, the outer $s$ -integration of [F4] turns the $t$ -inner integral into $ε / (ε^{2} + s^{2})$ , while the outer $t$ -integration turns the $s$ -inner integral into $e^{- ε t} \sin (t) / t$ ; hence $J_{ε} : = \int_{[0, \infty)} e^{- ε t} f (t) d λ (t)$ satisfies $J_{ε} = \int_{0}^{1} ε / (ε^{2} + s^{2}) d s$ , and [F15] with the substitution $s = ε v$ followed by [F16] gives $J_{ε} = \int_{0}^{1 / ε} d v / (1 + v^{2}) = \arctan (1 / ε)$ .

6.1step 4.2step 4.3step 5.1F17

Let $A \geq 1$ and $0 < ε \leq 1$ . By 4.2 and 4.3, $∣ S (A) - J_{ε} ∣ \leq ∣ S (A) - \int_{[0, A]} e^{- ε t} f d λ ∣ + 2 / A$ , so letting $ε ↓ 0$ and using 5.1 gives $∣ S (A) - π / 2 ∣ \leq 2 / A$ : indeed $\arctan (1 / ε) \to π / 2$ since [F17] makes $\arctan$ strictly increasing onto $(- π / 2, π / 2)$ , whence for every $v < π / 2$ one has $\arctan y > v$ for all $y > \tan v$ , while $\arctan (1 / ε) < π / 2$ always. Letting $A \to \infty$ yields $S (T) \to π / 2$ , so the improper integral $\int_{0}^{\infty} \sin (u) / u d u$ converges to $π / 2$ .

7.1step 3.2step 6.1F7F13F15F19∎

If $z = 0$ , the integrand with its assigned value at $t = 0$ is identically zero, and the identity, bound and limit follow directly, with $sgn (0) = 0$ . If $T = 0$ , both finite integrals vanish. For $z \neq 0$ and $T > 0$ , put $g (t) : = \sin (t z) / t$ for $t \neq 0$ , $g (0) : = z$ ; by [F7] and [F13], $g$ is continuous and even, so [F15] with the substitution $t \mapsto - t$ on $[0, T]$ and [F19] give $\int_{- T}^{T} g = 2 \int_{0}^{T} g$ . By [F15] with the substitution $u = ∣ z ∣ t$ (orientation retained, and $\sin (- u) / (- u) = \sin (u) / u$ by [F13]) and [F7], $\int_{0}^{T} g = sgn (z) \int_{0}^{T ∣ z ∣} \sin (u) / u d u = sgn (z) S (T ∣ z ∣)$ , so $\int_{- T}^{T} g = 2 sgn (z) S (T ∣ z ∣)$ ; step 3.2 bounds this by $6$ , and step 6.1 gives the limit $π sgn (z)$ .

Depends on

Used by

Dependency tree · two levels

118 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

Loukas Grafakos, Classical Fourier Analysis, third edition (standard reference, not scraped)
Richard S. Laugesen, Harmonic Analysis Lecture Notes (standard reference, not scraped)