QuantumInfo.ForMathlib.ComplexLaplaceTransform

Given a type $\alpha$ and an energy function $E: \alpha \to \mathbb{R} \cup \{+\infty\}$, for a complex number $z \in \mathbb{C}$ and an element $x \in \alpha$, the complex Laplace integrand is defined as $e^{-z E(x)}$ if $E(x) < +\infty$, and $0$ if $E(x) = +\infty$.

Given a measure space $\alpha$ and an energy function $E: \alpha \to \mathbb{R} \cup \{+\infty\}$, the complex Laplace transform at $z \in \mathbb{C}$ is defined as the integral over $\alpha$ of the function $e^{-z E(x)}$. For values where $E(x) = +\infty$, the integrand is defined to be $0$.

Given a measure space $\alpha$ and an energy function $E : \alpha \to \mathbb{R} \cup \{+\infty\}$, the complex convergence domain is the set of complex numbers $z \in \mathbb{C}$ such that the function $x \mapsto e^{-z E(x)}$ (where $e^{-z E(x)} = 0$ if $E(x) = +\infty$) is integrable with respect to the volume measure on $\alpha$.

Let $\alpha$ be a type and $E: \alpha \to \mathbb{R} \cup \{+\infty\}$ be a function. For any configuration $x \in \alpha$ and any complex number $z \in \mathbb{C}$, the complex Laplace integrand, defined as the function $w \mapsto e^{-w E(x)}$ when $E(x) < +\infty$ and $w \mapsto 0$ when $E(x) = +\infty$, is complex analytic at $z$.

Let $\alpha$ be a measurable space and let $E: \alpha \to \mathbb{R} \cup \{+\infty\}$ be a measurable function. For any complex number $z \in \mathbb{C}$, the complex Laplace integrand $x \mapsto e^{-z E(x)}$ (defined as $0$ when $E(x) = +\infty$) is a measurable function.

Let $\alpha$ be a measure space and $E: \alpha \to \mathbb{R} \cup \{+\infty\}$ be an energy function. Let the convergence domain of the complex Laplace transform be the set of complex numbers $z \in \mathbb{C}$ such that the function $x \mapsto e^{-z E(x)}$ is integrable with respect to the volume measure on $\alpha$ (where $e^{-z E(x)}$ is defined as $0$ when $E(x) = +\infty$). If a point $z$ lies in the interior of this convergence domain, then there exists a neighborhood of $z$ such that for every $w$ in that neighborhood, the function $x \mapsto e^{-w E(x)}$ is integrable.

Let $(\alpha, \mu)$ be a measure space and $E: \alpha \to \mathbb{R} \cup \{+\infty\}$ be an energy function. Let $\mathcal{L}(z) = \int_{\alpha} e^{-z E(x)} \, d\mu(x)$ denote the complex Laplace transform of $E$, where the integrand is defined to be $0$ whenever $E(x) = +\infty$. If a complex number $z \in \mathbb{C}$ belongs to the interior of the convergence domain of $\mathcal{L}$ (the set of points where the integrand is integrable), then the complex Laplace transform $\mathcal{L}$ is continuous at $z$.

Let $(\alpha, \mu)$ be a measure space and $E: \alpha \to \mathbb{R} \cup \{+\infty\}$ be an energy function. Let $\mathcal{D} \subseteq \mathbb{C}$ be the convergence domain of the complex Laplace transform, defined as the set of $z \in \mathbb{C}$ such that the function $x \mapsto e^{-z E(x)}$ (with the convention that $e^{-z E(x)} = 0$ if $E(x) = +\infty$) is integrable with respect to $\mu$. Then the complex Laplace transform $$z \mapsto \int_{\alpha} e^{-z E(x)} \, d\mu$$ is continuous on the interior of $\mathcal{D}$.

Let $(\alpha, \mu)$ be a measure space where $\mu$ is a $\sigma$-finite measure. Let $E: \alpha \to \mathbb{R} \cup \{+\infty\}$ be a measurable function, and let $D \subseteq \mathbb{C}$ be the convergence domain of the complex Laplace transform of $E$, defined as the set of complex numbers $z$ for which the function $x \mapsto e^{-z E(x)}$ is integrable (with $e^{-z E(x)} = 0$ when $E(x) = +\infty$). If $z$ lies in the interior of $D$, then the complex Laplace transform $F(z) = \int_{\alpha} e^{-z E(x)} \, d\mu(x)$ is analytic at $z$.