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

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.

Symmetry and the trigonometric form of the real Beta integral

Statement

For $p, q > 0$ , $B (p, q) = B (q, p) = 2 \int_{0}^{π / 2} \sin^{2 p - 1} θ \cos^{2 q - 1} θ d θ$ .

Facts & Assumptions

Given: Positive real parameters $p, q$ .

[F1]

If $ϕ : I \to J$ is a monotone differentiable surjection with locally integrable derivative, the proper change-of-variable hypotheses hold on every compact truncation, and $f$ is locally integrable on $J$ , then the improper integrals of $f$ and $f (ϕ) ∣ ϕ^{'} ∣$ converge simultaneously and are equal when convergent (Change of variable in an improper integral).

[F2]

The Beta integral converges if and only if $p > 0$ and $q > 0$ (Euler's Beta integral converges exactly for two positive parameters).

Proof

technique · direct

1.1

In the convergent integral [F2], the decreasing substitution $u = 1 - t$ interchanges $p$ and $q$ . By [F1], $B (p, q) = B (q, p)$ .

F1F2algebra

1.2

On compact interior truncations use $t = \sin^{2} θ$ , with $d t = 2 \sin θ \cos θ d θ$ and $1 - t = \cos^{2} θ$ . The transformed integrand is $2 \sin^{2 p - 1} θ \cos^{2 q - 1} θ$ .

F1F2algebra

2.1

Let the truncations tend to $0$ and $π / 2$ . Convergence from [F2] and [F1] yields the full trigonometric integral and completes the displayed equality.

step 1.2F1F2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

University of Toronto MAT237Y1, The Gamma Function and the Beta Function, §2.2(a) (standard reference, not scraped)