The real-line exponential tail is Lebesgue integrable

Given: Countable Choice, the natural numbers $\mathbb{N}$, and the function $f(x)=\exp (-\mathrm{\mid }x\mathrm{\mid })$.

Countable Choice is the set-theoretic assumption used by the continuous-to-Borel and box-measure results. The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)

The exponential is continuous, positive and strictly increasing, and satisfies $\exp (-x)=1\mathrm{/}\exp (x)$ for every real $x$. Continuous real functions on $\mathbb{R}$ are Borel measurable under Countable Choice. The exponential is positive and satisfies $\exp (-x)=1\mathrm{/}\exp (x)$, The exponential function is strictly increasing, Continuous functions on Euclidean spaces are Borel measurable

Every half-open interval $[a,b)$ is Lebesgue measurable with measure $b-a$. A box in ${\mathbb{R}}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure ${\prod }_{i<n}(b_i-a_i)$, whichever of its faces are included

The nonnegative Lebesgue integral is monotone, additive on nonnegative measurable functions, and satisfies monotone convergence. Monotonicity and nonnegative homogeneity of the nonnegative integral, Additivity of the nonnegative Lebesgue integral, Monotone convergence for the integral

If $0<r<1$, then ${\sum }_{k=0}^{\mathrm{\infty }}{r}^k=1\mathrm{/}(1-r)<\mathrm{\infty }$. For $\mathrm{\mid }r\mathrm{\mid }<1$, ${\sum }_{k\ge 0}{r}^k=1\mathrm{/}(1-r)$, and for $\mathrm{\mid }r\mathrm{\mid }\ge 1$ the series diverges

Arithmetic combinations of measurable real functions are measurable. Arithmetic and lattice operations preserve measurability whenever they are defined

The exponential addition formula, induction, and recursive integer-power definition give $\exp (-k)=\exp (-1{)}^k$ for every natural $k$. The exponential addition formula $\exp (x+y)=\exp (x)\exp (y)$, The principle of mathematical induction, Integer powers $a^m$

The nonnegative Lebesgue integral of a nonnegative measurable function is the supremum of the integrals of its nonnegative simple minorants. The nonnegative Lebesgue integral

The natural numbers $\mathbb{N}$ start at $0$ and are closed under successor. The natural numbers $\mathbb{N}$ (von Neumann)

A natural index used as a real endpoint is read through its canonical embedding into $\mathbb{R}$. The canonical natural $\iota (n)=n\cdot 1_F$ of a field

For a nonnegative measurable function and a measurable set $E$, ${\int }_{E}fd\lambda$ means $\int f{\mathbf{1}}_{E}d\lambda$. Integral over a measurable subset

Under Countable Choice, every Borel subset of $\mathbb{R}$ is Lebesgue measurable. Assuming countable choice, every Borel subset of ${\mathbb{R}}^n$ is Lebesgue measurable

The canonical naturals are cofinal in $\mathbb{R}$. Every complete ordered field is Archimedean

A nonnegative simple function has the same nonnegative Lebesgue and simple integrals; in particular, $\int c{\mathbf{1}}_{E}d{\lambda }_1=c{\lambda }_1(E)$ for $c\ge 0$ and measurable $E$ of finite measure. The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions