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.
The real Gamma function has one minimum and diverges at both ends of its domain
Statement
As , and . As , both and tend to . Moreover there is a unique at which attains its global minimum; it decreases on and increases on .
Facts & Assumptions
Given: The positive smooth function on and .
For every , , and (The real Gamma functional equation ).
The real Gamma function is strictly log-convex on (The real Gamma function is strictly log-convex).
The real Gamma function is smooth on (The real Gamma function is smooth and its derivatives are logarithmic moments).
For every natural , ( for every natural number ).
For a differentiable on an open interval, is convex if and only if is nondecreasing (A differentiable function on an open interval is convex if and only if its derivative is nondecreasing).
If is continuous on and differentiable on , then for some (The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with ); a function with positive derivative on an interval is increasing there and one with negative derivative is decreasing (On an interval , for continuous on and differentiable at every interior point: throughout gives nondecreasing, gives increasing, and give the two decreasing forms; conversely a nondecreasing has and a nonincreasing has wherever it is differentiable, and no strict converse is claimed).
Proof
By continuity at and [F1], as . Since , this also gives .
One has , while strict convexity [F2] gives for . Fixing such an and applying [F6] on and on gives with and with .
By [F2] and [F5], is nondecreasing. If for some , then is constant on , so is affine there, contradicting the strict convexity of [F2]; hence 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 . Strict increase makes negative before and positive after it, so [F6] makes , and hence , decreasing on and increasing on , and is the unique global minimum.
By [F4], . For , the ratios of grow by a factor exceeding , so this sequence tends to infinity. By the eventual increase from step 2.1, if then and . Thus both quantities tend to infinity.
Depends on
- The real Gamma functional equation $\Gamma(s+1)=s\Gamma(s)$
- $\Gamma(n+1)=n!$ for every natural number $n$
- The real Gamma function is smooth and its derivatives are logarithmic moments
- The real Gamma function is strictly log-convex
- A differentiable function on an open interval is convex if and only if its derivative is nondecreasing
- 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)$
- On an interval $I$, for $f$ continuous on $I$ and differentiable at every interior point: $f' \ge 0$ throughout gives $f$ nondecreasing, $f' > 0$ gives $f$ increasing, $f' \le 0$ and $f' < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f' \ge 0$ and a nonincreasing $f$ has $f' \le 0$ wherever it is differentiable, and no strict converse is claimed
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- For $|r| < 1$ the sequence $r^k$ is null, and for $|r| > 1$ the sequence $|r|^k$ diverges to $+\infty$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
71 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, §1.3(c,d) (standard reference, not scraped)