When are Feynman diagrams Borel summable I've been trying to understand Feynman diagrams more rigorously, and it seems that everything can be rigorously defined as long as the Feynman diagrams are Borel summable. However, are there any good indicators/lemmas of when a series of Feynman diagrams are Borel summable?
Indeed, consider the simple $\phi^4$ theory on a finite lattice $\Lambda \subseteq \mathbb{Z}^d$. Notice that exists a well-defined Gaussian measure $\mu_G$ on $\mathbb{Z}^d$ and thus it's possible to compute correlation functions $G_\lambda(x,y)$ with respect to the distribution
$$
\propto\exp\left(-\lambda \sum_{x\in \Lambda} \phi(x)^4\right) d\mu_G
$$
where $\lambda$ is the coupling constant. It's not to hard to check that $G_\lambda (x,y)$ is smooth (though not analytic) at $\lambda=0$ and it's Taylor series coefficients can be represented as Feynman diagrams, i.e., the terms $a_n \lambda^n$ are calculated using the Feynman diagrams.
Now if the series $\sum a_n\lambda^n$ were asymptotic to $G_\lambda (x,y)$ and also Borel summable, then the error of the first $N$ terms would just be $\propto N! \lambda^N$
A quick plot would see that this error is quite small for the first few terms if $\lambda>0$ is small.
Question. In general, I don't quite see why the formal series $\sum a_n\lambda^n$ is Borel summable to $G_\lambda (x,y)$? Is this at least true for the $\phi^4$ theory on a finite lattice $\Lambda$?
 A: Yes this theory is Borel summable even after taking the box $\Lambda$ to infinity.
To learn about these things look at the pedagogical paper "Constructive field theory in zero dimension" by Rivasseau.
Note that in principle to show a model is Borel summable, the naive procedure is to: 1) define the Borel transform, i.e., the function with power series coefficients given by the original ones divided by $n!$, 2) analytically continue in a strip around the positive real axis, 3) take an integral transform to recover the wanted function, i.e., some correlation function.
However, this almost never is how one proves Borel summability because step 2) is too hard to do if all one knows is the perturbation series. What is usually done is to construct the correlation by other means and then afterwards show that it is indeed the Borel sum of the perturbative series. This only requires some precise $n!$ remainder estimates. This is explained in the above article by Rivasseau.
For examples of QFT models without UV cutoff where this has been done in a mathematically rigorous way see the article by Eckmann, Magnen, Sénéor in CMP on $\phi^2$ in 2d, by Magnen and Sénéor on $\phi^4$ in 3d and by Feldman, Magnen, Rivasseau and Sénéor for massive Gross-Neveu in 2d as well as infrared $\phi^4$ in 4d.
