LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Weierstrass log-Gamma series converges to a Gamma branch

Statement

For every $z$ with $Re z > 0$ , the series defining $ℓ_{+} (z)$ in Log-Gamma branch on the right half-plane converges locally uniformly, defines a holomorphic function, and satisfies $e^{ℓ_{+} (z)} = Γ (z)$ for Euler's Gamma function on that half-plane.

Facts & Assumptions

Given: $Re z > 0$ and the definitions in Log-Gamma branch on the right half-plane.

[F1]

Euler's Beta function on the right half-planes: $B (p, q) = \int_{0}^{1} t^{p - 1} (1 - t)^{q - 1} d t (Re p, Re q > 0) .$

[F2]

The principal logarithm is the normalised holomorphic branch on the slit plane: ${Log}^{'} (w) = 1 / w$ and $\exp (Log w) = w$ on the slit plane.

[F3]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ and A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: a continuously differentiable real function integrates its derivative to its endpoint difference, and a continuous derivative on a compact interval is integrable; apply componentwise to complex-valued functions of a real parameter.

[F4]

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$ and 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)$ : addition commutes with the real integral, and pointwise order gives the corresponding integral bounds; apply to components of complex-valued integrands.

[F5]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t and Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\log^{'} (x) = 1 / x$ for $x > 0$ , $\log (x y) = \log x + \log y$ , and $\log 1 = 0$ .

[F6]

The complex exponential is entire and its complex derivative is itself, Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with $\partial_{\overset{ˉ}{z}} f = 0$ , or with the Cauchy–Riemann equations, and The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : the complex exponential is real-totally differentiable with derivative multiplication by its value, so the real-parameter derivative of $t \mapsto \exp (z \log t)$ is $z t^{z - 1}$ . $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential gives the addition law; Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ supplies the product rule used for $t^{z} (1 - t)^{N}$ . The same complex-to-real derivative correspondence and total chain rule apply to the holomorphic principal logarithm along the affine real-parameter paths in step 1.1.

[F7]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ : for $u > 0$ , $∣ u^{z - 1} ∣ = u^{Re z - 1}$ under the real-log power convention.

[F8]

Euler's Gamma function on the right half-plane and Euler's Gamma integral converges locally uniformly on the right half-plane: for $Re z > 0$ , $Γ (z) = \int_{0}^{\infty} u^{z - 1} e^{- u} d u$ , and the corresponding positive real majorant is integrable.

[F9]

The Euler-Mascheroni constant and The Euler–Mascheroni constant and the harmonic asymptotic: if $H_{N} = \sum_{n = 1}^{N} 1 / n$ , then $H_{N} - \log N \to γ$ .

[F10]

The exponential function is strictly increasing, The exponential function is smooth and $(\exp)^{'} = \exp$ , and Mean value theorem on a closed real interval: the real exponential is increasing, has derivative $e^{x}$ , and its mean-value estimate applies on compact intervals.

[F11]

Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly: a locally uniform limit of holomorphic functions is holomorphic.

[F12]

Change of variable in an improper integral: monotone affine changes of variable preserve the corresponding proper and improper integrals; apply componentwise to the complex Beta integrand.

Proof

1.1givenF2F3F6F11algebra

For $w = z / n$ with $Re z > 0$ , the path $1 + t w$ lies in the principal-logarithm domain. Its derivative integrand is continuous on $[0, 1]$ and is integrable by [F3]. By [F2], [F3], and the real-parameter chain rule, $Log (1 + w) = \int_{0}^{1} \frac{w}{1 + t w} d t, w - Log (1 + w) = \int_{0}^{1} \frac{t w^{2}}{1 + t w} d t .$ Since $∣ 1 + t w ∣^{2} = 1 + 2 t Re w + t^{2} ∣ w ∣^{2} \geq 1$ , the summand has absolute value at most $∣ z ∣^{2} / (2 n^{2})$ . Summing this bound is uniform on every compact subset of the right half-plane. Each summand is holomorphic there, so the series converges locally uniformly and defines a holomorphic function by [F11].

1.2F1F3F4F6algebrainduction

For $N \geq 1$ , the Beta integrals satisfy $B (z, 1) = \frac{1}{z}, B (z, N + 1) = \frac{N}{z + N} B (z, N) .$ For the base formula, apply [F3] componentwise on $[ε, 1]$ to the primitive $t^{z} / z$ and let $ε ↓ 0$ ; the lower boundary tends to $0$ since $∣ ε^{z} ∣ = ε^{Re z}$ . For $N \geq 1$ , differentiate $g (t) = t^{z} (1 - t)^{N}$ on $[ε, 1]$ . By [F6], $g^{'} (t) = z t^{z - 1} (1 - t)^{N} - N t^{z} (1 - t)^{N - 1} .$ The derivative is continuous and integrable on this compact interval by [F3]. Applying the componentwise fundamental theorem and then letting $ε ↓ 0$ gives $z B (z, N + 1) = N B (z + 1, N)$ ; both boundary terms vanish. The integrand identity $t^{z - 1} (1 - t)^{N - 1} = t^{z - 1} (1 - t)^{N} + t^{z} (1 - t)^{N - 1}$ and [F4] give $B (z, N) = B (z, N + 1) + B (z + 1, N)$ . Combining these two equalities yields $(z + N) B (z, N + 1) = N B (z, N)$ , proving the recurrence. Iterating it from $B (z, 1) = 1 / z$ gives $B (z, N + 1) = \frac{N!}{z (z + 1) \dots (z + N)} .$ All denominators are nonzero because $Re (z + j) > 0$ for $j \geq 0$ .

1.3F5F9F10F12algebra

Fix $z$ with $a : = Re z > 0$ , and define $K_{N} (u) = (1 - u / N)^{N}$ for $0 \leq u \leq N$ and $K_{N} (u) = 0$ for $u > N$ . For $0 \leq u < N$ , [F5] and [F12] give $\log (1 - u / N) = - \int_{0}^{u / N} \frac{d s}{1 - s} \leq - \frac{u}{N},$ so $0 \leq K_{N} (u) \leq e^{- u}$ by exponential monotonicity and the addition law; the same bound holds at $u = N$ . On a fixed interval $[0, R]$ , for $N > 2 R$ , $N \log (1 - u / N) = - u - δ_{N} (u), 0 \leq δ_{N} (u) = N \int_{0}^{u / N} \frac{s}{1 - s} d s \leq \frac{R^{2}}{N} .$ The mean value theorem in [F10] and $e^{t} \leq 1$ for $t \leq 0$ give $∣ K_{N} (u) - e^{- u} ∣ \leq R^{2} / N$ uniformly on $[0, R]$ .

2.1F1F5F12step 1.2algebra

Define $A_{N} (z) : = \frac{N! N^{z}}{z (z + 1) \dots (z + N)}, N^{z} : = \exp (z \log N) .$ By step 1.2 and the substitution $u = N t$ in [F12], $A_{N} (z) = N^{z} B (z, N + 1) = \int_{0}^{N} u^{z - 1} {(1 - \frac{u}{N})}^{N} d u .$ The real logarithm laws in [F5] preserve the stated power convention under this substitution.

2.2F4F7F8step 1.3algebra

By [F7], $∣ u^{z - 1} ∣ = u^{a - 1}$ . For each real or imaginary component, the integral difference on $[0, R]$ is bounded, using [F4], by $\frac{R^{2}}{N} \int_{0}^{R} u^{a - 1} d u = \frac{R^{a + 2}}{a N} .$ On $[R, \infty)$ , $K_{N} (u) \leq e^{- u}$ bounds the difference in each component by $2 \int_{R}^{\infty} u^{a - 1} e^{- u} d u$ , which tends to $0$ as $R \to \infty$ by [F8]. First choosing $R$ large and then $N$ large proves $A_{N} (z) \to Γ (z)$ .

3.1F2F6F8F9step 1.1step 1.2step 2.1step 2.2algebra∎

Let $ℓ_{N} (z)$ be the defining partial sum through $N$ and put $P_{N} (z) : = z \exp (γ_{E} z) \prod_{n = 1}^{N} (1 + \frac{z}{n}) e^{- z / n} .$ The principal-log identity $\exp (Log w) = w$ , the exponential addition law in [F6], and the formula from step 1.2 give $\exp (ℓ_{N} (z)) = P_{N} (z)^{- 1}, P_{N} (z) A_{N} (z) = \exp ⁣ (z (γ_{E} + \log N - H_{N})) .$ By [F9] the second expression tends to $1$ . By step 1.1, $ℓ_{N} (z) \to ℓ_{+} (z)$ ; continuity of the complex exponential gives $P_{N} (z) \to \exp (- ℓ_{+} (z))$ . Step 2.2 gives $A_{N} (z) \to Γ (z)$ , so $\exp (- ℓ_{+} (z)) Γ (z) = 1.$ Multiplying by $\exp (ℓ_{+} (z))$ and using the addition law proves $e^{ℓ_{+} (z)} = Γ (z)$ .

Depends on

Used by

Cited to discharge well-definedness by Log-Gamma branch on the right half-plane.

Dependency tree · two levels

140 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

DLMF, §5.2, Gamma function and Euler constant (standard reference, not scraped)
DLMF, §5.8(ii), equation 5.8.2 (standard reference, not scraped)
N. M. Temme, “Numerical aspects of special functions,” Acta Numerica 17 (2008), §§2 and 3 (standard reference, not scraped)