LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Wallis integrals satisfy the two-step recurrence, closed forms, and the adjacent-integral squeeze

Statement

For $n \in N$ , put

$I_{n} : = \int_{0}^{π / 2} \sin^{n} t d t .$

Then $I_{0} = π / 2$ , $I_{1} = 1$ , and for every $n \geq 2$ ,

$I_{n} = \frac{n - 1}{n} I_{n - 2} .$

Consequently, for every $m \geq 0$ ,

$I_{2 m} = \frac{π}{2} \prod_{k = 1}^{m} \frac{2 k - 1}{2 k}, I_{2 m + 1} = \prod_{k = 1}^{m} \frac{2 k}{2 k + 1},$

where an empty product is $1$ . For $m \geq 1$ ,

$I_{2 m + 1} \leq I_{2 m} \leq I_{2 m - 1}, 1 \leq \frac{I_{2 m}}{I_{2 m + 1}} \leq \frac{2 m + 1}{2 m},$

and therefore $I_{2 m} / I_{2 m + 1} \to 1$ .

Facts & Assumptions

Given: The functions $t \mapsto \sin^{n} t$ on $[0, π / 2]$ and the integrals $I_{n}$ .

[L1]

Integration by parts gives $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ when the stated derivatives are integrable (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$ ).

[L2]

$(\sin t)^{'} = \cos t$ , $(\cos t)^{'} = - \sin t$ , $\sin 0 = 0$ , $\cos 0 = 1$ , and $\sin^{2} t + \cos^{2} t = 1$ (The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine).

[L3]

Sine is strictly increasing on $[- π / 2, π / 2]$ , has range $[- 1, 1]$ , and satisfies $\sin (π / 2) = 1$ and $\cos (π / 2) = 0$ (Signs, monotonicity intervals, and ranges of sine and cosine, Quarter-turn values and shifts by pi/2 and pi).

[L4]

The integral is linear; the integral of a constant $c$ on $[a, b]$ is $c (b - a)$ ; and if $f \leq g$ pointwise on $[a, b]$ then $\int_{a}^{b} f \leq \int_{a}^{b} g$ (Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ , If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ , If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[L5]

A finite product in a monoid has empty product equal to the identity and satisfies the recursion that adjoins its last factor (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity).

[L6]

A sequence squeezed between two sequences with the same limit has that limit (The squeeze theorem).

[L7]

The constant $π$ is positive (Pi as twice the smallest positive zero of cosine).

Proof

technique · direct

1.1

By [L3] and [L4], $I_{0} = \int_{0}^{π / 2} 1 d t = π / 2$ , while [L2] gives $I_{1} = [- \cos t]_{0}^{π / 2} = 1$ .

L2L3L4algebra

1.2

Let $n \geq 2$ . Apply [L1] to $u = \sin^{n - 1} t$ and $v^{'} = \sin t$ . The endpoint term $[- \sin^{n - 1} t \cos t]_{0}^{π / 2}$ is $0$ , including the first legal case $n = 2$ , and [L2] gives $I_{n} = (n - 1) \int_{0}^{π / 2} \sin^{n - 2} t \cos^{2} t d t .$

givenL1L2L3algebra

1.3

For $m \geq 1$ , [L2] and [L3] give $0 \leq \sin^{2 m + 1} t \leq \sin^{2 m} t \leq \sin^{2 m - 1} t$ , so the integral bounds in [L4] yield $I_{2 m + 1} \leq I_{2 m} \leq I_{2 m - 1}$ .

L2L3L4

2.1

Substitute $\cos^{2} t = 1 - \sin^{2} t$ in step 1.2 and use [L4]: $I_{n} = (n - 1) (I_{n - 2} - I_{n})$ , hence $I_{n} = ((n - 1) / n) I_{n - 2}$ .

step 1.2L2L4algebra

3.1

Iterating step 2.1 separately from the base values of step 1.1 gives the displayed even and odd product formulas; when $m = 0$ , [L5] makes them exactly $I_{0} = π / 2$ and $I_{1} = 1$ .

step 1.1step 2.1L5algebra

4.1

All $I_{j}$ are positive by the product formulas in step 3.1: their base values are positive by [L7], and every displayed factor is positive. Dividing step 1.3 by $I_{2 m + 1}$ and using step 2.1 at $n = 2 m + 1$ gives $1 \leq \frac{I_{2 m}}{I_{2 m + 1}} \leq \frac{I_{2 m - 1}}{I_{2 m + 1}} = \frac{2 m + 1}{2 m} .$

step 2.1step 1.3step 3.1L7algebra

5.1

Both outer sequences in step 4.1 tend to $1$ , so [L6] gives $I_{2 m} / I_{2 m + 1} \to 1$ .

step 4.1L6∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 131 results over 32 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

D. Galvin, Primitives and techniques of integration, section 13.2 (standard reference, not scraped)
Imperial College London, History of Mathematics, Problems VI solutions (standard reference, not scraped)