Alphabeta Math
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.

✓ 22 results · all verified · 10 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 12 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Real Gamma and Beta Functions

1 · Prerequisites

2 · Summary

Improper integration supplies convergence, comparison, exhaustion, and dominated parameter differentiation, while logarithms and real powers control endpoint singularities and parameter derivatives. One-variable convexity supplies secant-slope inequalities, and the Gaussian integral and Wallis product give independent real routes to the constant π. The ball-volume recursion provides the geometric input for the dimension formula.

Euler's Gamma and Beta integrals are first shown to converge on their exact positive domains. The Gamma recurrence gives factorial values, dominated differentiation gives smoothness, and strict log-convexity yields Gautschi's inequality and, through a factorial squeeze, Bohr--Mollerup uniqueness. A first-quadrant change of variables proves the Beta--Gamma identity. Gaussian and Wallis arguments separately evaluate Γ(1/2), Wallis fixes the constant in Stirling's formula, and the Beta identity closes the unit-ball volume formula, its radius scaling, limiting behavior, and maximizing dimension.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Log-convex positive functions

Definition

A positive function f:I→(0,∞) is log-convex when log⁡∘f is convex on I.

Equivalently, for x,y∈I and 0≤λ≤1 with (1−λ)x+λy∈I,

f((1−λ)x+λy)≤f(x)1−λf(y)λ.

It is strictly log-convex when this inequality is strict for x≠y and 0<λ<1. Positivity ensures that every logarithm and every real power in these formulas is defined.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The real Gamma function by Euler's integral

Definition

For s>0, define Γ(s)=∫0∞ts−1e−t dt.

The integral is improper at both 0 and +∞. Its convergence for every s>0, and its failure for s≤0, are proved in Euler's Gamma integral converges exactly for positive real parameters ↗, which justifies the definition on exactly the displayed domain. The integrand is positive, so Γ(s)>0 throughout (0,∞).

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Euler's Gamma integral converges exactly for positive real parameters

Statement

Let s be real. The Euler integral ∫0∞ts−1e−t dt converges if and only if s>0.

Facts & Assumptions

Given: A real parameter s, with the integral split at 1.

[F1]

For every natural m and real a>0, xm/exp⁡(ax)→0 as x→+∞ (The exponential dominates every fixed nonnegative integer power at +∞).

[F2]

If 0≤u≤v eventually at a singular end and the improper integral of v converges there, then the integral of u converges; the same assertion holds separately at infinity and at either finite singular endpoint (Comparison tests for improper integrals).

[F3]

For x>0, log⁡′(x)=1/x and log⁡x=∫1xdt/t (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[F4]

The natural logarithm is strictly increasing and maps (0,∞) onto R (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F5]

For real α, xα is differentiable on (0,∞) with derivative αxα−1 (Continuity and derivatives of positive-base real powers).

Proof

technique · direct
1.1givenF2F5algebra

Suppose s>0. On (0,1], e−1≤e−t≤1, and [F5] with the fundamental theorem gives ∫01ts−1 dt=1/s<∞. Thus [F2] gives convergence at zero.

1.2givenF2F3F4cases

If s≤0, then ts−1≥t−1 on (0,1], while e−t≥e−1. At s=0 this is exactly the logarithmic threshold, and [F3] and [F4] show ∫01dt/t diverges; the same lower comparison proves divergence for s<0.

1.3F1F2choose

For arbitrary real s, choose a natural m≥max⁡{s−1,0}. For t≥1, ts−1e−t≤tme−t, and [F1] with a=1/2 makes tme−t≤e−t/2 eventually. Since the latter has a convergent improper integral, [F2] gives convergence at infinity.

2.1step 1.1step 1.2step 1.3cases-exhaustive∎

Steps 1.1 and 1.3 prove convergence for s>0, while step 1.2 proves divergence for every s≤0. Hence the two improper ends converge simultaneously exactly on the positive real axis.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Euler's real Beta integral

Definition

For p,q>0, define B(p,q)=∫01tp−1(1−t)q−1 dt.

The integral is improper at both endpoints. The exact convergence theorem Euler's Beta integral converges exactly for two positive parameters ↗ proves that it exists precisely for the displayed positive parameters and therefore discharges the definition's existence obligation.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Euler's Beta integral converges exactly for two positive parameters

Statement

Let p,q be real. The Beta integral converges if and only if p>0 and q>0.

Here the Beta integral means ∫01tp−1(1−t)q−1 dt.

Facts & Assumptions

Given: Real parameters p,q, with the integral split at 1/2.

[F1]

If 0≤u≤v eventually at a finite singular endpoint and the improper integral of v converges there, then the integral of u converges (Comparison tests for improper integrals).

[F2]

For x>0, log⁡′(x)=1/x and log⁡x=∫1xdt/t (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[F3]

The natural logarithm is strictly increasing and maps (0,∞) onto R (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F4]

For real α, xα is differentiable on (0,∞) with derivative αxα−1 (Continuity and derivatives of positive-base real powers).

Proof

technique · direct
1.1givenF1F2F3F4algebra

On (0,1/2], the continuous positive factor (1−t)q−1 is bounded above and below by positive constants. Thus [F1] reduces convergence at zero to that of ∫01/2tp−1 dt, whose primitive from [F4] converges exactly for p>0; at p=0, [F2] and [F3] give logarithmic divergence, and for p<0 the integrand dominates the same threshold.

1.2givenF1F2F3F4algebra

The substitution u=1−t changes the end t↑1 into u↓0. There tp−1 is bounded above and below by positive constants, so [F4] and the same comparison give convergence exactly for q>0, with logarithmic divergence at q=0.

2.1step 1.1step 1.2algebra∎

Both endpoint integrals converge exactly when p>0 and q>0. If either parameter is nonpositive, the corresponding endpoint diverges by step 1.1 or step 1.2.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

The real Gamma functional equation Γ(s+1)=sΓ(s)

Statement

For every s>0, Γ(s+1)=sΓ(s), and Γ(1)=1.

Facts & Assumptions

Given: A real parameter s>0 and truncation parameters 0<ε<1<R.

[F1]

If differentiable u,v on a compact interval have integrable derivatives, then ∫uv′=uv∣ab−∫u′v (If u,v are differentiable on [a,b] with u′,v′ integrable, then ∫abuv′=u(b)v(b)−u(a)v(a)−∫abu′v).

[F2]

The Euler integral converges if and only if its real parameter is positive (Euler's Gamma integral converges exactly for positive real parameters).

Proof

technique · direct
1.1givenF1

Apply [F1] on [ε,R] with u(t)=ts and v′(t)=e−t: ∫εRtse−t dt=[−tse−t]εR+s∫εRts−1e−t dt.

2.1step 1.1algebra

Since s>0, εse−ε→0 as ε↓0. At infinity choose a natural m>s; then Rse−R≤Rme−R→0 by exponential domination.

3.1step 1.1step 2.1F2

Letting the two truncations approach their improper ends in step 1.1 and using [F2] gives Γ(s+1)=sΓ(s).

4.1F2algebra∎

At s=1, Γ(1)=∫0∞e−t dt=[−e−t]0∞=1.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Γ(n+1)=n! for every natural number n

Statement

For every natural number n, Γ(n+1)=n!.

Facts & Assumptions

Given: Factorial recursion 0!=1 and (n+1)!=(n+1)n! from The factorial n! and the falling factorial nk‾, defined by recursion in N.

[F1]

For every s>0, Γ(s+1)=sΓ(s), and Γ(1)=1 (The real Gamma functional equation Γ(s+1)=sΓ(s)).

Proof

technique · induction
1.1F1base

At n=0, [F1] gives Γ(1)=1=0!.

1.2F1ihalgebra

Assume Γ(n+1)=n!. Then [F1] gives Γ(n+2)=(n+1)Γ(n+1)=(n+1)n!=(n+1)!.

2.1step 1.1step 1.2discharge-induction∎

The induction principle therefore proves Γ(n+1)=n! for every n∈N.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

The real Gamma function is smooth and its derivatives are logarithmic moments

Statement

The real Gamma function is smooth on (0,∞). For every natural k and every s>0, Γ(k)(s)=∫0∞(log⁡t)kts−1e−t dt.

Facts & Assumptions

Given: A compact parameter interval [a,b]⊂(0,∞) and a natural derivative order k.

[F1]

If an integrand and its parameter derivative are continuous, one slice is absolutely improperly integrable, and on each compact parameter interval the derivative has a nonnegative improperly integrable uniform bound, then the integral is continuously differentiable and its derivative is the integral of the parameter derivative (Differentiation under an improper multiple integral under an integrable derivative bound).

[F2]

For every natural m and real a>0, xm/exp⁡(ax)→0 as x→+∞ (The exponential dominates every fixed nonnegative integer power at +∞).

[F3]

If a property holds at 0 and passes from n to n+1, then it holds for every natural n (The principle of mathematical induction).

[F4]

The Euler integral converges for every positive real parameter (Euler's Gamma integral converges exactly for positive real parameters).

Proof

technique · direct
1.1givenF2construct

On (0,1], put u=−log⁡t. Uniformly for s∈[a,b], the absolute kth parameter derivative becomes uke−su≤uke−au after substitution. By [F2] this is eventually bounded by e−au/2 and is integrable.

1.2givenF2construct

On [1,∞), s≤b and log⁡t≤t allow ∣(log⁡t)kts−1e−t∣ to be bounded by tme−t for one natural m depending only on b,k. By [F2] this has an integrable exponential majorant.

2.1step 1.1step 1.2F1F3F4

The case k=0 is the defining integral, convergent by [F4] and absolutely convergent because its integrand is nonnegative. If the displayed formula holds at order k, its integrand and parameter derivative are continuous; steps 1.1 and 1.2, applied at orders k and k+1, give one absolutely integrable slice and an integrable uniform derivative bound. Thus [F1] differentiates once more. By [F3], the formula holds for every natural k.

3.1step 2.1∎

Every s>0 lies in a compact interval [a,b]⊂(0,∞), so step 2.1 proves the formulas and smoothness throughout the positive axis.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

The real Gamma function is strictly log-convex

Statement

The real Gamma function is strictly log-convex on (0,∞).

Facts & Assumptions

Given: Distinct x,y>0 and a weight 0<λ<1.

[F1]

For 0<λ<1, exponential convexity is strict unless its two arguments are equal (The two-point convexity inequality for the exponential function).

[F2]

A positive function is log-convex when its logarithm is convex (Log-convex positive functions).

Proof

technique · direct
1.1givenF1

Fix c>0 and write csΓ(s)=∫0∞t−1e−texp⁡(slog⁡(ct)) dt. By [F1], the integrand at (1−λ)x+λy is at most the corresponding convex combination, with strict inequality except at the single point t=1/c; integration makes s↦csΓ(s) strictly convex.

1.2constructalgebra

Choose c=(Γ(x)/Γ(y))1/(y−x)>0. Then cxΓ(x)=cyΓ(y).

2.1step 1.1step 1.2F2algebra∎

Apply step 1.1 at x,y with the c from step 1.2. After cancelling c(1−λ)x+λy, one gets Γ((1−λ)x+λy)<Γ(x)1−λΓ(y)λ, which is strict log-convexity by [F2].

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

The real Gamma function has one minimum and diverges at both ends of its domain

Statement

As s↓0, sΓ(s)→1 and Γ(s)→+∞. As s→+∞, both Γ(s) and Γ(s)/s tend to +∞. Moreover there is a unique s0∈(1,2) at which Γ attains its global minimum; it decreases on (0,s0] and increases on [s0,∞).

Facts & Assumptions

Given: The positive smooth function Γ on (0,∞) and g:=log⁡Γ.

[F1]

For every s>0, Γ(s+1)=sΓ(s), and Γ(1)=1 (The real Gamma functional equation Γ(s+1)=sΓ(s)).

[F2]

The real Gamma function is strictly log-convex on (0,∞) (The real Gamma function is strictly log-convex).

[F3]

The real Gamma function is smooth on (0,∞) (The real Gamma function is smooth and its derivatives are logarithmic moments).

[F4]

For every natural n, Γ(n+1)=n! (Γ(n+1)=n! for every natural number n).

[F5]

For a differentiable f on an open interval, f is convex if and only if f′ is nondecreasing (A differentiable function on an open interval is convex if and only if its derivative is nondecreasing).

Proof

technique · direct
1.1F1algebra

By continuity at 1 and [F1], sΓ(s)=Γ(s+1)→Γ(1)=1 as s↓0. Since s→0+, this also gives Γ(s)→+∞.

1.2F2F6algebra

One has g(1)=g(2)=0, while strict convexity [F2] gives g(x)<0 for 1<x<2. Fixing such an x and applying [F6] on [1,x] and on [x,2] gives ξ∈(1,x) with g′(ξ)<0 and η∈(x,2) with g′(η)>0.

2.1step 1.2F2F3F5F6

By [F2] and [F5], g′ is nondecreasing. If g′(u)=g′(v) for some u<v, then g′ is constant on [u,v], so g is affine there, contradicting the strict convexity of [F2]; hence g′ is strictly increasing and has at most one zero. By [F3] it is continuous, so the sign change in step 1.2 gives exactly one zero s0∈(1,2). Strict increase makes g′ negative before s0 and positive after it, so [F6] makes g, and hence Γ, decreasing on (0,s0] and increasing on [s0,∞), and s0 is the unique global minimum.

3.1step 2.1F4algebra∎

By [F4], Γ(n+1)=n!. For n≥3, the ratios of (n−1)!/(n+1) grow by a factor exceeding 2, so this sequence tends to infinity. By the eventual increase from step 2.1, if n≤s<n+1 then Γ(s)≥Γ(n)=(n−1)! and Γ(s)/s≥(n−1)!/(n+1). Thus both quantities tend to infinity.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Gautschi's inequality for the real Gamma function

Statement

For x>0 and 0≤s≤1, x1−s≤Γ(x+1)/Γ(x+s)≤(x+1)1−s.

For 0<s<1 both inequalities are strict. At s=0 the lower inequality is equality, and at s=1 both are equalities.

Facts & Assumptions

Given: A real x>0 and 0≤s≤1.

[F1]

The real Gamma function is strictly log-convex on (0,∞) (The real Gamma function is strictly log-convex).

[F2]

For every x>0, Γ(x+1)=xΓ(x) (The real Gamma functional equation Γ(s+1)=sΓ(s)).

Proof

technique · direct
1.1givenF1

Log-convexity between x and x+1 gives Γ(x+s)≤Γ(x)1−sΓ(x+1)s=xsΓ(x), strictly when 0<s<1.

1.2givenF1

Since x+1=s(x+s)+(1−s)(x+s+1), log-convexity gives Γ(x+1)≤Γ(x+s)sΓ(x+s+1)1−s=(x+s)1−sΓ(x+s)≤(x+1)1−sΓ(x+s).

2.1step 1.1step 1.2F2algebra∎

Divide the inequalities in steps 1.1 and 1.2 by positive Gamma values and use [F2]. This gives the displayed bounds and the stated strictness. Direct substitution shows the lower equality at s=0 and both equalities at s=1.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Log-convex solutions of the Gamma recurrence obey the Bohr--Mollerup factorial squeeze

Statement

Let f:(0,∞)→(0,∞) be log-convex, with f(1)=1 and f(x+1)=xf(x) for every x>0. For 0<x≤1 and every integer n≥2, put

Gn(x):=nxn!x(x+1)⋯(x+n).

Then

Gn(x)≤f(x)≤n+xnGn(x).

Every positive log-convex f with f(1)=1 and f(x+1)=xf(x) lies between the Bohr--Mollerup factorial bounds, whose ratio is (n+x)/n for 0<x≤1.

Facts & Assumptions

Given: Such a function f, a real 0<x≤1, and an integer n≥2.

[F1]

A positive function is log-convex exactly when its logarithm is convex (Log-convex positive functions).

[F2]

Factorial is determined by 0!=1 and (n+1)!=(n+1)n! (The factorial n! and the falling factorial nk‾, defined by recursion in N).

[F3]

For a convex f on an interval, writing s(a,b)=(f(b)−f(a))/(b−a), one has s(x,y)≤s(x,z)≤s(y,z) whenever x<y<z lie in it (For a convex function and x<y<z, the three secant slopes satisfy s(x,y)≤s(x,z)≤s(y,z)).

Proof

technique · direct
1.1givenF1F3cases

By [F1] the function log⁡f is convex, and the recurrence with f(n)=(n−1)! makes its secant slopes s(n−1,n)=log⁡(n−1) and s(n,n+1)=log⁡n. For 0<x<1, [F3] at n−1<n<n+x gives s(n−1,n)≤s(n,n+x) and [F3] at n<n+x<n+1 gives s(n,n+x)≤s(n,n+1); at x=1 the middle slope is s(n,n+1)=log⁡n itself and log⁡(n−1)≤log⁡n. Either way log⁡(n−1)≤(log⁡f(n+x)−log⁡f(n))/x≤log⁡n, and exponentiation yields (n−1)x(n−1)!≤f(n+x)≤nx(n−1)!.

1.2givenF2

Iterating the recurrence gives f(n+x)=x(x+1)⋯(x+n−1)f(x) and, by induction from [F2], f(n)=(n−1)!.

2.1step 1.1step 1.2algebra∎

Divide the bounds of step 1.1 by the positive product in step 1.2. Use the upper bound at n and the lower bound with n replaced by n+1; both then have the common term Gn(x), and they become Gn(x)≤f(x)≤((n+x)/n)Gn(x).

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Bohr--Mollerup characterisation of the real Gamma function

Statement

Gamma is the unique positive log-convex function f:(0,∞)→(0,∞) with f(1)=1 and f(x+1)=xf(x).

Facts & Assumptions

Given: The real Gamma function and an arbitrary positive log-convex function f satisfying the displayed normalization and recurrence.

[F1]

Every such function lies between common factorial bounds whose ratio is (n+x)/n for 0<x≤1 (Log-convex solutions of the Gamma recurrence obey the Bohr--Mollerup factorial squeeze).

[F2]

For every s>0, Γ(s+1)=sΓ(s), and Γ(1)=1 (The real Gamma functional equation Γ(s+1)=sΓ(s)).

[F3]

The real Gamma function is strictly log-convex on (0,∞) (The real Gamma function is strictly log-convex).

[F4]

Every real lies in a unique half-open unit interval between consecutive integers (Integer part: for every real x there is exactly one integer m with m≤x<m+1).

Proof

technique · direct
1.1F2F3

Gamma is positive by its Euler integrand, normalized and recurrent by [F2], and log-convex by [F3]. Thus it satisfies the characterizing properties.

2.1F1step 1.1algebra

Fix 0<x≤1. Apply [F1] to f and to Gamma. Both lie between Gn(x) and ((n+x)/n)Gn(x) for every n≥2, and the ratio of these bounds tends to 1. The squeeze theorem therefore gives f(x)=Γ(x).

3.1step 2.1F2F4

By [F4], every positive real y is an integer shift of a unique x∈(0,1]. Iterating the common recurrence from [F2] and the hypothesis on f extends the equality of step 2.1 from that strip to y.

4.1step 1.1step 2.1step 3.1∎

Step 1.1 proves that Gamma has the properties, and steps 2.1 and 3.1 prove that every function with them equals Gamma. This is the claimed characterization.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

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.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The real Beta--Gamma identity

Statement

For p,q>0, B(p,q)=Γ(p)Γ(q)/Γ(p+q).

Facts & Assumptions

Given: Positive reals p,q and the nonnegative function xp−1yq−1e−(x+y) on the open first quadrant.

[F1]

If f:D→[0,∞) is locally Riemann integrable and (Kj) is a compact Jordan exhaustion, then ∫Df=sup⁡j∫Kjf, independently of the exhaustion (Every Jordan exhaustion computes a nonnegative improper multiple integral).

[F2]

If g:U→Rn is injective and C1 with invertible derivative on an open set, K⊆U is compact Jordan, and f is bounded on g(K), then f is integrable exactly when (f∘g)∣det⁡Dg∣ is, and their integrals are equal (Change of variables for an injective C1 map on a compact Jordan set).

[F3]

If A,B are nondegenerate closed rectangles, f is integrable on A×B, and every section in one coordinate order is integrable, then the ordinary iterated integral in that order exists and equals the multiple integral (Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections).

Proof

technique · direct
1.1F1F3

On compact rectangles inside the first quadrant, [F3] factors the integral as a product of one-variable integrals. Passing through rectangular exhaustion by [F1] gives total improper integral Γ(p)Γ(q).

1.2F2algebra

On compact rectangles inside (0,∞)×(0,1) use x=rt, y=r(1−t). The map is injective, its absolute Jacobian is r, and [F2] transforms the integrand times Jacobian into rp+q−1e−rtp−1(1−t)q−1.

2.1step 1.1step 1.2F1F3

A fixed nested family of such compact rectangles maps to a cofinal exhaustion of the first quadrant. By [F1] the limit is independent of this exhaustion, and by [F3] the transformed integral factors as Γ(p+q)B(p,q).

3.1step 2.1algebra∎

Gamma is positive on the positive axis, so division of the equality in step 2.1 by Γ(p+q) gives the claimed identity.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The elementary recurrences for the real Beta function

Statement

For p,q>0,

B(p+1,q)=pp+qB(p,q),B(p,q+1)=qp+qB(p,q),

and consequently B(p,q)=B(p+1,q)+B(p,q+1).

Facts & Assumptions

Given: Positive real parameters p,q.

[F1]

For p,q>0, B(p,q)=Γ(p)Γ(q)/Γ(p+q) (The real Beta--Gamma identity).

[F2]

For every s>0, Γ(s+1)=sΓ(s) (The real Gamma functional equation Γ(s+1)=sΓ(s)).

Proof

technique · direct
1.1F1F2algebra

By [F1] and [F2], B(p+1,q)=Γ(p+1)Γ(q)/Γ(p+q+1)=pB(p,q)/(p+q).

1.2F1F2algebra

Similarly, B(p,q+1)=qB(p,q)/(p+q).

2.1step 1.1step 1.2algebra∎

Adding steps 1.1 and 1.2 and using p+q>0 gives B(p+1,q)+B(p,q+1)=B(p,q).

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Γ(1/2)=π from the Gaussian integral

Statement

Γ(1/2)=π.

Facts & Assumptions

Given: Euler's Gamma integral at s=1/2.

[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 Gaussian integral is ∫−∞∞e−x2 dx=π (The Gaussian integral ∫−∞∞e−x2 dx=π).

Proof

technique · direct
1.1F1algebra

In Γ(1/2)=∫0∞t−1/2e−t dt, use t=u2 on proper truncations. By [F1], the improper limit is 2∫0∞e−u2 du.

2.1step 1.1F2algebra

The integrand is even, so splitting [F2] at zero shows 2∫0∞e−u2 du=π.

3.1step 2.1∎

Combining the two identities gives Γ(1/2)=π, with the positive square root selected because Gamma is positive.

Remarks

The independent Wallis-product route is Γ(1/2)=π by Wallis's product.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Γ(1/2)=π by Wallis's product

Statement

Γ(1/2)=π.

Facts & Assumptions

Given: Positive integers n tending to infinity.

[F1]

For x>0 and 0≤s≤1, x1−s≤Γ(x+1)/Γ(x+s)≤(x+1)1−s (Gautschi's inequality for the real Gamma function).

[F2]

If an=(2nn)/4n, then πn an→1 (The central binomial coefficient is asymptotic to 4^n divided by the square root of pi n).

[F4]

For every s>0, Γ(s+1)=sΓ(s) (The real Gamma functional equation Γ(s+1)=sΓ(s)).

Proof

technique · direct
1.1F4algebra

Iterating [F4] gives Γ(n+1/2)=Γ(1/2)∏k=0n−1(k+1/2)=((2n)!/(4nn!))Γ(1/2), with the empty product valid at n=0.

1.2F1

Apply [F1] with x=n and s=1/2. After inversion, n/(n+1)≤n Γ(n+1/2)/n!≤1, so this middle sequence tends to 1.

2.1step 1.1step 1.2F2F3algebra

By step 1.1 and [F3], the middle sequence is Γ(1/2)n(2nn)/4n. Fact [F2] makes its limit Γ(1/2)/π, while step 1.2 makes the same limit 1.

3.1step 2.1∎

Positivity of Gamma and uniqueness of limits therefore give Γ(1/2)=π.

Remarks

This proof uses Gautschi and Wallis. The Gaussian-integral proof Γ(1/2)=π from the Gaussian integral is logically independent of it.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Stirling's factorial asymptotic holds up to a positive constant

Statement

There is a constant C>0 such that n!∼Cn(n/e)n. Here n tends to infinity through the positive integers.

Facts & Assumptions

Given: Positive integers r,n and the logarithm on positive reals.

[F1]

For −1<x≤1, log⁡(1+x)=∑j=1∞(−1)j+1xj/j (The power series for log(1+x), including the Abel endpoint).

[F2]

The positive series ∑k≥1k−p converges exactly when p>1 (The p-series for a real exponent p converges exactly when p is greater than one).

Proof

technique · direct
1.1F1algebra

Put er:=log⁡r−∫r−1/2r+1/2log⁡t dt. After t=r+u, expand log⁡(1+u/r) by [F1]. Integration over the symmetric interval cancels the odd powers, and the remaining absolutely convergent even series gives ∣er∣≤K/r2 for one constant K and all r≥1.

2.1step 1.1F2

By step 1.1 and [F2] with p=2, the series ∑r≥1er converges absolutely.

3.1step 2.1F3algebra

Summing the definition of er from 1 to n telescopes the integrals to ∫1/2n+1/2log⁡t dt. Fact [F3] gives the primitive tlog⁡t−t, and comparison of n+1/2 with n shows that log⁡(n!)−((n+1/2)log⁡n−n) converges to a real constant c.

4.1step 3.1algebra∎

Exponentiating step 3.1 and putting C=ec>0 gives n!/(n(n/e)n)→C, which is the stated asymptotic.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Wallis's product determines the Stirling constant as 2π

Statement

The constant C in the preceding asymptotic is 2π.

Facts & Assumptions

Given: The positive constant C from the preceding lemma.

[F1]

There is a constant C>0 such that n!∼Cn(n/e)n (Stirling's factorial asymptotic holds up to a positive constant).

[F2]

The Wallis consequence is (2nn)∼4n/πn (The central binomial coefficient is asymptotic to 4^n divided by the square root of pi n).

Proof

technique · direct
1.1F1F3algebra

Insert the two asymptotics of [F1] into the quotient [F3]. Cancellation gives (2nn)∼(2/C)4n/n.

2.1step 1.1F2algebra∎

Comparing the positive leading coefficient in step 1.1 with [F2] gives 2/C=1/π. Since C>0, C=2π.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Stirling's formula for factorials

Statement

n!∼2πn(n/e)n as the positive integer n tends to infinity.

Equivalently,

n!2πn(n/e)n⟶1(n→∞, n≥1).

Facts & Assumptions

Given: Positive integer n tending to infinity.

[F1]

There is a constant C>0 such that n!∼Cn(n/e)n (Stirling's factorial asymptotic holds up to a positive constant).

[F2]

The constant C in that asymptotic is 2π (Wallis's product determines the Stirling constant as 2π).

Proof

technique · direct
1.1F1F2algebra

Insert [F2] into [F1] and combine 2πn=2πn.

2.1step 1.1∎

By the definition of asymptotic equivalence, step 1.1 is exactly the displayed ratio limit. The restriction n≥1 keeps its denominator positive.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

The closed form for the volume of the unit n-ball

Statement

For every n≥1, Vn(1)=πn/2/Γ(n/2+1). Here n is an integer.

Facts & Assumptions

Given: Unit-ball volumes Vn(1) in positive integer dimensions.

[F1]

One has V1(r)=2r for r≥0, and for n≥2, Vn(1)=Vn−1(1)∫−11(1−t2)(n−1)/2 dt (Closed Euclidean balls are Jordan measurable and their volumes satisfy the slicing recursion).

[F2]

For p,q>0, B(p,q)=Γ(p)Γ(q)/Γ(p+q) (The real Beta--Gamma identity).

[F4]

For s>0, Γ(s+1)=sΓ(s) (The real Gamma functional equation Γ(s+1)=sΓ(s)).

Proof

technique · induction
1.1F1F3F4basealgebra

In dimension 1, [F1] gives V1(1)=2, while [F3] and [F4] give π1/2/Γ(3/2)=π/((1/2)π)=2.

1.2ihF1F2F3algebra

Assume the formula in dimension n−1. In the integral of [F1], symmetry followed by u=t2 gives ∫−11(1−t2)(n−1)/2 dt=B(1/2,(n+1)/2). By [F2] and [F3], this equals π Γ((n+1)/2)/Γ(n/2+1).

2.1step 1.2discharge-inductionalgebra∎

Multiply the expression in step 1.2 by the induction value π(n−1)/2/Γ((n+1)/2); the common Gamma factor cancels, giving Vn(1)=πn/2/Γ(n/2+1). This discharges the induction.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

The volume of a radius-r closed n-ball is πn/2rn/Γ(n/2+1)

Statement

For n≥1 and r≥0, Vn(r)=πn/2rn/Γ(n/2+1), where n is an integer.

Facts & Assumptions

Given: Positive integer n and radius r≥0.

[F1]

One has V1(r)=2r for r≥0, and for n≥2 and r≥0, Vn(r)=Vn−1(1)∫−rr(r2−t2)(n−1)/2 dt (Closed Euclidean balls are Jordan measurable and their volumes satisfy the slicing recursion).

[F2]

For every n≥1, Vn(1)=πn/2/Γ(n/2+1) (The closed form for the volume of the unit n-ball).

Proof

technique · direct
1.1givencases

If r=0, the ball is a singleton of content zero, and the right side is zero because n≥1.

1.2F1algebra

Suppose r>0. For n=1, V1(r)=2r=rV1(1). For n≥2, substitute t=ru in [F1]; the power and differential contribute rn−1 and r, so comparison with [F1] at radius 1 gives Vn(r)=rnVn(1).

2.1step 1.1step 1.2F2cases-exhaustive∎

Insert [F2] into step 1.2 and combine it with the zero-radius case of step 1.1. This gives the displayed formula for every allowed n,r.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The volume of the unit n-ball tends to zero with dimension

Statement

Vn(1)→0 as n→∞. The limit is through the positive integers.

Facts & Assumptions

Given: The positive sequence of unit-ball volumes Vn:=Vn(1).

[F1]

For every n≥1, Vn=πn/2/Γ(n/2+1) (The closed form for the volume of the unit n-ball).

[F2]

For every s>0, Γ(s+1)=sΓ(s) (The real Gamma functional equation Γ(s+1)=sΓ(s)).

Proof

technique · direct
1.1F1F2algebra

From [F1] and [F2], Vn+2/Vn=2π/(n+2) for every n≥1.

2.1step 1.1F3algebra

Choose an integer threshold after which 2π/(n+2)≤1/2. Along each parity chain, step 1.1 then bounds every later volume by a fixed initial volume times successive powers of 1/2, which tend to zero by [F3].

3.1step 2.1∎

Both the odd-dimensional and even-dimensional subsequences tend to zero, so their interleaving (Vn) also tends to zero.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The unit-ball volume is maximal in dimension five

Statement

Among positive integer dimensions, the unit-ball volume is uniquely maximal at n=5.

Facts & Assumptions

Given: Unit-ball volumes Vn:=Vn(1) for positive integers n.

[F1]

For every n≥1, Vn=πn/2/Γ(n/2+1) (The closed form for the volume of the unit n-ball).

[F2]

For every natural N, the Gregory--Leibniz formula writes π/4 as its partial sum through N plus a signed remainder of magnitude at most 1/(2N+3) (The Gregory-Leibniz series: pi over four equals 1-1/3+1/5-1/7+...).

[F3]

For every s>0, Γ(s+1)=sΓ(s), and Γ(1)=1 (The real Gamma functional equation Γ(s+1)=sΓ(s)).

Proof

technique · direct
1.1F2algebra

In [F2], the partial sum through N=7 is 33976/45045>3/4 and its remainder is positive, so π>3. The partial sum through N=18 is 133330680156299/166966608033225<4/5 and its remainder is negative, so π<16/5.

2.1F1F3step 1.1algebra

Facts [F1] and [F3] give Vn+2/Vn=2π/(n+2). Using step 1.1, the odd chain increases through V5 and then decreases, while the even chain increases through V6 and then decreases.

2.2F1F3F4step 1.1algebra

From [F3], Γ(7/2)=(5/2)(3/2)(1/2)Γ(1/2)=(15/8)π by [F4], and Γ(4)=3⋅2⋅1⋅Γ(1)=6. Hence [F1] gives V5=π5/2/((15/8)π)=8π2/15 and V6=π3/6. The upper bound π<16/5 from step 1.1 gives V5>V6.

3.1step 2.1step 2.2∎

Step 2.1 identifies the unique maximum within each parity chain, and step 2.2 compares the two candidates. Therefore V5 is the unique global maximum.

5 · Examples, counterexamples and false statements

None yet.

Sources