Let a quantum system with a single degree of freedom be given. We want to define the path integral so that we get the representation for the propagator as
$$\langle q' |e^{-iHT}|q\rangle=\int_{x(a)=q, x(b)=q'} \mathcal{D}x(t) e^{iS[x(t)]}.$$
Now, I want to make sure I understand how this integration is defined in more rigorous terms. My issue is that most texts seem to just define that particular integral above (of $e^{iS[x(t)]}$) but for me, to define a path integral would mean define what we mean for a functional to be integrable and define how it would be integrated, the above being just one case.
So I've tried to extract the actual definition from Peskin's QFT book and I want to verify if I got it right.
So in summary we want to define the integral of a functional $\mathfrak{F}[x(t)]$
$$\int \mathfrak{F}[x(t)] \mathcal{D}x(t).$$
After reading a few times what Peskin does, I came up with the following:
Definition: Let $[a,b]\subset \mathbb{R}$ and let a partition $P$ of $[a,b]$ be given: $$a=t_0<t_1<\cdots<t_{N-1}<t_N=b.$$ Let $x_0,\dots, x_{N}\in \mathbb{R}$. We call the piecewise smooth path $x : [a,b]\to \mathbb{R}$ given by $$x(t)=x_k+\frac{x_{k+1}-x_k}{t_{k+1}-t_k}(t-t_k),\quad t\in [t_{k},t_{k+1}],\quad k\in \{0,\dots, N\}$$ a linear interpolation of the points $x_0,\dots, x_N$.
Definition: Let $C_p^{\infty}([a,b];\mathbb{R})$ be the space of piecewise smooth paths defined in $[a,b]$. Let further $\mathfrak{F}: C_p^\infty([a,b];\mathbb{R})\to \mathbb{C}$ be a given functional acting on such paths.
Let further $P$ be a partition of $[a,b]$ into $N$ subintervals. We define the functional $\mathfrak{F}_P : \mathbb{R}^{N+1}\to \mathbb{C}$ with respect to this partition to be
$$\mathfrak{F}_P(x_0,\dots,x_N)=\mathfrak{F}[x_P(t)]$$
where $x_P(t)$ is the linear interpolation of the points $x_0,\dots, x_N$.
Definition: Let $C^\infty_p([a,b];\mathbb{R})$ be the space of piecewise smooth paths defined in $[a,b]$. Let a functional $\mathfrak{F}: C^\infty_p([a,b];\mathbb{R})\to \mathbb{C}$ be given.
We say that $\mathfrak{F}$ is functionally integrable if the limit:
$$\lim_{|P|\to 0}\int_{\mathbb{R}^{N+1}} \mathfrak{F}_P(x_0,\dots, x_N) dx_0\cdots dx_{N}$$
exists, where $|P|$ is the mesh of the partition, given by $$|P|=\max\{t_{k+1}-t_k | k\in \{0,\dots, N\}\}.$$ In that case we call such limit the functional integral of $\mathfrak{F}$ and denote it by
$$\int \mathcal{D}x(t) \mathfrak{F}[x(t)].$$
So is that the mathematically idea behind it? In the end for Phyics we would be interested in the case $\mathfrak{F}[x(t)]=e^{iS[x(t)]}$.
So in that process I think that the crucial step is:
The time-slice procedure together with the linear interpolation construction allows us to turn a functional $\mathfrak{F}$ into an ordinary function which obviously depend on the particular time-slicing (the partition).
The function can be integrated giving a result that depends on the partition. We then study the limit as the mesh goes to zero.
The thing with analytic continuation, Wick rotation and euclidean action, would then appear just for the specific functional $e^{iS[x(t)]}$ in order to get something that is functionally integrable.
Have I got it right? Is this the actual mathematically precise version of what is done in most QM/QFT texts?
If not, where did I got it wrong or what did I miss?
