LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Complex Gaussian continuation

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). For $z \in C$ with $Re z > 0$ and $n \geq 1$ let

$G_{n} (z) : = \int_{R^{n}} e^{- z ∣ x ∣^{2}} d x,$

where $d x$ is product Lebesgue measure and the complex integral is computed from its real and imaginary parts. Equivalently, the absolutely convergent improper multiple integral used here is the cube-truncation limit $\lim_{R \to \infty} \int_{[- R, R]^{n}} e^{- z ∣ x ∣^{2}} d x$ of these finite Lebesgue integrals. For $n = 1$ it also equals the sum of the two separately convergent one-sided improper Riemann integrals at $0$ , computed componentwise (Improper integrals over unbounded intervals); this agreement is proved below. Then:

(a) $G_{n} (z)$ converges absolutely for every $z$ with $Re z > 0$ , and $G_{1}$ is holomorphic on the right half-plane $Ω : = {z \in C : Re z > 0}$ with $G_{1}^{'} (z) = - \int_{R} x^{2} e^{- z x^{2}} d x$ (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions, A complex domain is a nonempty connected open subset of $C$ );

(b) with $Log$ the principal logarithm and the branch $z^{- 1 / 2} : = \exp (- \frac{1}{2} Log z)$ on the slit plane (Complex logarithms, the principal logarithm, and principal and multivalued complex powers, The principal logarithm is the normalised holomorphic branch on the slit plane),

$G_{1} (z) = \sqrt{π} z^{- 1 / 2}, G_{1} (z)^{2} = \frac{π}{z} (z \in Ω),$

the value on the positive real axis being $G_{1} (t) = \sqrt{π / t}$ for $t > 0$ ;

(c) for every $n \geq 1$ and $z \in Ω$ , $G_{n} (z) = G_{1} (z)^{n} = (π / z)^{n / 2}$ , the power being the branch $(π / z)^{n / 2} = \exp (\frac{n}{2} (\log π - Log z))$ .

In particular the factor $(1 + i τ)^{- 1 / 2}$ is defined by this branch for every real $τ$ , since $Re (1 + i τ) = 1 > 0$ . No asymptotic or distributional interpretation is asserted.

Facts & Assumptions

Given: $n \geq 1$ ; a complex parameter $z$ with $Re z > 0$ ; the functions $G_{n}$ of the Statement; the principal logarithm $Log$ .

[F1]

For $n \geq 1$ , $t > 0$ and $ξ \in R^{n}$ , $F (e^{- π t ∣ x ∣^{2}}) (ξ) = t^{- n / 2} e^{- π ∣ ξ ∣^{2} / t}$ ; at $ξ = 0$ this reads $\int_{R^{n}} e^{- π t ∣ x ∣^{2}} d x = t^{- n / 2}$ , and substituting $s = π t$ gives $\int_{R^{n}} e^{- s ∣ x ∣^{2}} d x = (π / s)^{n / 2}$ . Every polynomial times a positive real Gaussian is absolutely integrable (Euclidean Gaussian transform with the 2π normalization).

[F2]

On a fixed measure space, if measurable complex-valued $f_{n}, f$ satisfy $f_{n} \to f$ almost everywhere and $∣ f_{n} ∣ \leq g$ almost everywhere for one nonnegative measurable $g$ with $\int g < \infty$ , then $\int ∣ f_{n} - f ∣ \to 0$ (Dominated convergence). For a parameter $h \to 0$ , apply this to each sequence of nonzero parameters tending to zero.

[F3]

A function is holomorphic when it is complex differentiable at every point of its domain; the derivative is the limit of difference quotients (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions). A complex domain is a nonempty connected open set (A complex domain is a nonempty connected open subset of $C$ ).

[F4]

The principal logarithm $Log$ is holomorphic on the slit plane $S = C ∖ (- \infty, 0]$ , satisfies $\exp (Log z) = z$ and $Log z = \log ∣ z ∣ + i Arg z$ with $Arg z \in (- π, π)$ , and $Log t = \ln t$ for $t > 0$ ; complex powers are defined by $z^{a} = \exp (a Log z)$ (Complex logarithms, the principal logarithm, and principal and multivalued complex powers, The principal logarithm is the normalised holomorphic branch on the slit plane).

[F5]

If two holomorphic functions on a complex domain agree on a set with an accumulation point in the domain, they agree everywhere (Identity theorem for holomorphic functions).

[F6]

Tonelli's theorem: for a product-measurable nonnegative function on a $σ$ -finite product, the iterated and double integrals agree (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F7]

For continuous $f : R^{n} \to C$ with $\int ∣ f ∣ < \infty$ , the improper multiple integral used here is $\lim_{R \to \infty} \int_{[- R, R]^{n}} f$ , with finite Lebesgue integrals computed componentwise. Dominated convergence (Dominated convergence) applied to $1_{[- R, R]^{n}} f$ identifies this limit with the product Lebesgue integral: for any sequence $R_{j} \to \infty$ the indicators tend pointwise to $1$ and are dominated by $∣ f ∣$ , hence every such sequence has the same limit. For $n = 1$ , the real and imaginary parts are bounded and Riemann integrable on every compact interval by A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, and their finite Riemann and Lebesgue integrals agree by A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral. Applying dominated convergence separately to $1_{[0, R]} f$ as $R \to \infty$ and $1_{[R, 0]} f$ as $R \to - \infty$ therefore proves convergence of both one-sided improper integrals of Improper integrals over unbounded intervals; the same argument for $∣ f ∣$ proves absolute convergence. Their sum is the full integral because the overlap ${0}$ has Lebesgue measure zero. Existence of a symmetric limit alone does not imply this agreement.

Proof

1.1givenF1F7algebra

[Absolute convergence] Let $z \in Ω$ and $δ : = Re z > 0$ . For every $x$ , $∣ e^{- z ∣ x ∣^{2}} ∣ = e^{- δ ∣ x ∣^{2}}$ , whose integral over $R^{n}$ is finite by [F1] with $s = δ$ ; hence the real and imaginary parts of $x \mapsto e^{- z ∣ x ∣^{2}}$ are absolutely improperly integrable and $G_{n} (z)$ is well defined by [F7]. The same bound holds uniformly on compact subsets of $Ω$ , where $δ$ can be taken positive uniformly.

2.1step 1.1F2F3F7algebra

[Holomorphy of $G_{1}$ ] Fix $z \in Ω$ and $0 < δ < Re z$ ; let $∣ h ∣ < δ / 2$ . For the function $w \mapsto e^{w}$ the second-order Taylor remainder satisfies $∣ e^{w} - 1 - w ∣ \leq ∣ w ∣^{2} e^{∣ w ∣}$ (the power series of $e^{w} - 1 - w$ has its first term $\frac{w^{2}}{2}$ and the remaining terms are bounded by $\frac{∣ w ∣^{2}}{2} (e^{∣ w ∣} - 1) \leq ∣ w ∣^{2} e^{∣ w ∣}$ ). Applying this with $w = - h x^{2}$ gives $∣ e^{- z x^{2}} \frac{e^{- h x^{2}} - 1 + h x^{2}}{h} ∣ \leq ∣ h ∣ x^{4} e^{(∣ h ∣ - Re z) x^{2}} \leq ∣ h ∣ x^{4} e^{- δ x^{2} / 2}$ for all real $x$ and all $∣ h ∣ < δ / 2$ , and $x \mapsto x^{4} e^{- δ x^{2} / 2}$ has finite integral; the remainder functions are continuous, hence measurable, converge pointwise to zero, and for $∣ h ∣ < δ / 2$ are dominated by the nonnegative integrable function $(δ / 2) x^{4} e^{- δ x^{2} / 2}$ . By [F2] along every sequence $h \to 0$ , their integrals over $R$ tend to zero. Thus the difference quotient $(G_{1} (z + h) - G_{1} (z)) / h$ tends, as $h \to 0$ , to $- \int_{R} x^{2} e^{- z x^{2}} d x$ . Hence $G_{1}$ is complex differentiable at every $z \in Ω$ , with the displayed derivative; by [F3] it is holomorphic on $Ω$ .

2.2step 1.1F1F3F4algebra

[The candidate branch] Put $H (z) : = \sqrt{π} \exp (- \frac{1}{2} Log z)$ for $z$ in the slit plane $S \supseteq Ω$ . By [F4], $Log$ is holomorphic on $S$ with ${Log}^{'} z = 1 / z$ , and the complex exponential is entire with derivative itself, so by the chain rule for complex derivatives $H$ is holomorphic on the complex domain $S$ (The chain rule for complex derivatives, The complex exponential is entire and its complex derivative is itself); also $H (z)^{2} = π \exp (- Log z) = π / z$ because $\exp (Log z) = z$ . On the positive axis, $Log t = \ln t$ [F4], so $H (t) = \sqrt{π} t^{- 1 / 2} = \sqrt{π / t}$ , which equals $G_{1} (t) = \int_{R} e^{- t x^{2}} d x$ by [F1] with $n = 1$ , $s = t$ .

3.1step 2.1step 2.2F3F5algebra

[Agreement by the identity theorem] The right half-plane $Ω$ is nonempty, open and convex (if $Re z_{1}, Re z_{2} > 0$ then $Re ((1 - λ) z_{1} + λ z_{2}) > 0$ for $0 \leq λ \leq 1$ ), hence a complex domain, and it is contained in $S$ , so both $G_{1}$ (step 2.1) and $H$ (step 2.2) are holomorphic on $Ω$ . They agree at every $t > 0$ (step 2.2), and the set $(0, \infty)$ has accumulation points in $Ω$ ; by [F5] applied to the complex domain $Ω$ , $G_{1} = H$ on $Ω$ , giving clause (b).

4.1step 3.1F4F6algebra∎

[Factorization] For $z \in Ω$ write $e^{- z ∣ x ∣^{2}} = \prod_{j = 1}^{n} e^{- z x_{j}^{2}}$ ; the absolute value factors as $\prod_{j} e^{- Re (z) x_{j}^{2}}$ , a product of nonnegative integrable functions of the single coordinates. Tonelli's theorem [F6] applied to the nonnegative function $x \mapsto \prod_{j} e^{- Re (z) x_{j}^{2}}$ shows that the multiple integral of $∣ e^{- z ∣ x ∣^{2}} ∣$ factorizes as the product of the one-dimensional integrals and is finite; hence $x \mapsto e^{- z ∣ x ∣^{2}}$ is integrable on the product, and the Fubini theorem for $L^{1}$ functions (Fubini's theorem for L^1 functions on a sigma-finite product) applied to its real and imaginary parts gives $G_{n} (z) = \prod_{j = 1}^{n} G_{1} (z) = G_{1} (z)^{n}$ . By step 3.1, $G_{1} (z)^{n} = (π / z)^{n / 2}$ in the branch notation of [F4]. This is clause (c), and $Re (1 + i τ) = 1 > 0$ shows the branch is defined at $1 + i τ$ .

Complex Gaussian continuation

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources