I am looking for a good reference about the analogues of the Bochner Theorem and the Lévy Continuity Theorem for probability measures on $\mathbb{R}^{\mathbb{N}}$ with the product topology.

Let $\mathscr{s}_0=\oplus_{\mathbb{N}}\mathbb{R}$, i.e, the space of sequences $x=(x_1,x_2,\ldots)$ of real numbers with only finitely many nonzero terms. One can view this as a locally convex topological vector space using the finest locally convex topology, namely, the one defined by the set of all seminorms one can put on it. The strong dual is naturally identified with the previous product space so I will simply write $\mathscr{s}'_0=\mathbb{R}^{\mathbb{N}}$ and use the duality pairing $$ \langle y,x\rangle=\sum_{n=1}^{\infty}y_n x_n $$ for all sequences $y\in \mathscr{s}'_0$ and $x\in\mathscr{s}$. Given a Borel probability measure $\mu$ on $\mathscr{s}'_0$ one defines the corresponding characteristic function $\Phi_{\mu}:\mathscr{s}_0\rightarrow \mathbb{C}$ with the usual formula $$ \Phi_{\mu}(x)=\int_{\mathscr{s}'_0} e^{i \langle y,x\rangle}\ d\mu(y) $$ Bochner's Theorem says that $\mu\rightarrow\Phi_{\mu}$ is a 1-to-1 correspondence between Borel probability measures on the countable product $\mathbb{R}^{\mathbb{N}}$ and functions $\Phi$ which satisfy: $\Phi(0)=1$, continuity at 0 in $\mathscr{s}_0$, and the usual positive type condition.

Lévy's Theorem says that a sequence of probability measures $(\mu_k)_{k\ge 1}$ converges weakly in $\mathbb{R}^{\mathbb{N}}$ if and only if their characteristic functions $\Phi_{\mu_k}$ converge pointwise to some function $\mathscr{s}_0\rightarrow \mathbb{C}$ that is continuous at the origin.

Bochner's Theorem follows almost trivially from the very classic finite dimensional one (I got plenty of good references for that) and the Daniell-Kolmogorov Extension Theorem. The "almost" is because one has to work a little to show continuity of characteristic functions because $\mathscr{s}_0$ is not metrizable (it is thankfully sequential).

For Lévy's Theorem this amounts to proving: weak convergence in the infinite product space $\mathbb{R}^{\mathbb{N}}$ is equivalent to the weak convergence of the finite-dimensional marginal. Is there a good proof somewhere of this last fact. I looked at some standard probability textbooks and the classic by Billingsley but did not see this. I suppose I could try to imbed $\mathbb{R}^{\mathbb{N}}$ in the space $D[0,\infty)$ of cadlag functions considered by Billingsley, using functions that are constant on intervals $[n,n+1)$ but this seems a bit excessive to me.