Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck 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∫0π/2sin⁡2p−1θcos⁡2q−1θ dθ.

Facts & Assumptions

Given: Positive real parameters p,q.

[F1]

If ϕ:I→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.1F1F2algebra

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

1.2F1F2algebra

On compact interior truncations use t=sin⁡2θ, with dt=2sin⁡θcos⁡θ dθ and 1−t=cos⁡2θ. The transformed integrand is 2sin⁡2p−1θcos⁡2q−1θ.

2.1step 1.2F1F2∎

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

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