Weak convergence for discrete-time processes using characteristic functions 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: 1) $\Phi(0)=1$, 2) continuity at 0 in $\mathscr{s}_0$, 3) for all $n\ge 1$ and elements $x^{(1)},\ldots,x^{(n)}$ in $\mathscr{s}_0$ the matrix $\left(\ \Phi(x^{(i)}-x^{(i)})\ \right)_{1\le i,j\le n}$ is positive semidefinite.
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, rather surprisingly, 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 marginals.
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.
As I said in a comment below what matters most to me is a reference for the statement in bold. If your reference is a book, please give a precise pointer like "Theorem 2.31 in ref X".
 A: If the process you concern is a harmonizable process then Bochner Theorem can be easily generalized into discrete time case by regarding it as Fourier representation. And in some more specific cases Doob's classic contains a lot of results/result pointers.

Doob, Joseph L., and Joseph L. Doob. Stochastic processes. Vol. 7. No.
  2. New York: Wiley, 1953.

Since Bochner's theorem worked basically for stationary processes, another classic is 

Ibragimov, Ilʹdar Abdulovich. "Independent and stationary sequences of
  random variables." (1971).

There is one book that discussed these issues you mentioned in OP in a slightly novel way (compared to the classic probability language), which is 

Friz, Peter K., and Nicolas B. Victoir. Multidimensional stochastic
  processes as rough paths: theory and applications. Vol. 120. Cambridge
  University Press, 2010.

In this book they use local estimate to approximate the discrete time behavior using a "finite-element" method, so their method can actually be applied to discrete case.
A: I finally found a book which does exactly what I need: "Probability Distributions on Linear Spaces" by N. N. Vakhania, North-Holland Publishing Co., 1981. Bochner's Theorem is done Section 1.2.2 and the Lévy Continuity Theorem is done in Section 1.2.8
As for the classics on weak convergence of probability measures I found a result in Ethier and Kurtz "Markov Processes, Characterization and Convergence" (1986 edition) which immediately implies the statement in bold. It is Theorem 4.5 on Page 113 together with the easy observation that bounded continuous functions that factor through finite-dimensional projections form a strongly separating set. In fact, although I did not catch that earlier, Billingsley (1999 edition) also has the needed result in Example 2.4 using a similar idea, although, I prefer convergence-determining continuous functions (as in EK) rather than sets (as in B).
