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.
Uniform sine integral bound and dirichlet value
Statement
Assume AC. Define for , with the integrand assigned value one at zero. Then is uniformly bounded and . For every real , and these integrals are bounded by one absolute constant for all and all . The integrand at is .
Facts & Assumptions
Given: The hypotheses and conventions in the statement.
Integration by parts applies to continuously differentiable factors on compact intervals. If are differentiable on with integrable, then .
An integrable derivative integrates to the endpoint increment. The second fundamental theorem: if is differentiable on with and is integrable, then .
Under countable choice compact Riemann and Lebesgue integrals agree. A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral.
Absolute integrability permits reversal of integration. Fubini's theorem for L^1 functions on a sigma-finite product.
Dominated convergence applies on each bounded u interval. Dominated convergence.
Sine and cosine have their usual derivatives, including sin derivative one at zero. The derivatives of sine and cosine are cosine and minus sine.
The derivative of the real exponential is itself. The exponential function is smooth and .
The chain rule differentiates the damped trigonometric primitive. The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with .
Arctangent evaluates the rational integral. Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series.
Arctangent increases onto its principal interval. The principal inverse tangent .
Oriented substitution applies to continuous integrands. Substitution: if is differentiable on with integrable and is continuous on an interval containing , then .
MVT bounds the sine increment by the derivative bound. The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with .
Sine and cosine have absolute value at most one. , , and .
AC supplies countable choice in the integral bridge. The Axiom of Choice.
Continuous compact-interval integrands are Riemann integrable. A continuous function on is Riemann integrable, by Heine-Cantor and Riemann's criterion.
Proof
The derivative of sine at zero makes . MVT and give , so the extended quotient is continuous and bounded by one on . It has a proper integral on every bounded interval. AC supplies the countable choice needed to identify these with Lebesgue integrals using F3 (and the compact integration interface F15).
For and , put . This is positive, decreasing, and continuously differentiable on , with . Integration by parts against gives At this proves the Cauchy property of as and the bound for all . For positive damping it also bounds the infinite tail by .
Fix . FTC gives , including . The double absolute integral of on is at most , so Fubini applies. Differentiating gives ; its limit at infinity is zero and its value at zero is . Consequently
On , dominated convergence gives convergence of the damped integral to as . The two tails, damped and undamped, are each at most by step 2.1. Thus, first taking and then , . The increasing inverse arctangent has limit at infinity: its values are below , and for every in its range, implies . Hence .
For the symmetric integral is zero. For , evenness in and substitution give Its absolute value is at most six, and for each fixed nonzero its limit is . The uniform bound, but not uniform convergence in z, is asserted.
Depends on
- 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$
- 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)$
- A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- Dominated convergence
- The Axiom of Choice
- Dirichlet's test for improper integrals
- Fubini's theorem for L^1 functions on a sigma-finite product
- The derivatives of sine and cosine are cosine and minus sine
- The exponential function is smooth and $(\exp)'=\exp$
- 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)$
- Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series
- Substitution: if $\varphi$ is differentiable on $[c,d]$ with $\varphi'$ integrable and $f$ is continuous on an interval containing $\varphi([c,d])$, then $\int_{\varphi(c)}^{\varphi(d)} f = \int_c^d (f\circ\varphi)\,\varphi'$
- A continuous function on $[a,b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion
- The principal inverse tangent $\arctan:\mathbb R\to(-\pi/2,\pi/2)$
- The mean value theorem, as the case $g(x) = x$ of Cauchy's: for $f$ continuous on $[a,b]$ with $a < b$ and differentiable on $(a,b)$ there is $c \in (a,b)$ with $f(b) - f(a) = f'(c)(b-a)$
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
Used by
- Levy inversion formula Theorem
Dependency tree · two levels
115 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
- Durrett, Probability: Theory and Examples, fifth edition (standard reference, not scraped)
- Norris, Probability and Measure (standard reference, not scraped)