Added FTC for path integrals.

src/fa/rs/index.tex

@@ -5,5 +5,6 @@
 \input{./bv.tex}
 \input{./rs.tex}
 \input{./rs-bv.tex}
+\input{./path.tex}
 \input{./regulated.tex}
 \input{./rs-measure.tex}

src/fa/rs/path.tex

@@ -0,0 +1,99 @@
+\section{Path Integrals}
+\label{section:path-integrals}
+
+\begin{definition}[Rectifiable Path]
+\label{definition:rectifiable-path}
+    Let $[a, b] \subset \real$, $F$ be a locally convex space over $K \in \RC$, and $\gamma \in C([a, b]; F)$ be a path, then $\gamma$ is \textbf{rectifiable} if $\gamma \in BV([a, b]; F)$.
+\end{definition}
+
+\begin{definition}[Path Integral]
+\label{definition:path-integral}
+    Let $[a, b] \subset \real$, $E, F, H$ be locally convex spaces over $K \in \RC$, $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous bilinear map, and $\gamma \in C([a, b]; F)$ be a path. For any $f: \gamma([a, b]) \to E$, $f$ is \textbf{path-integrable with respect to $\gamma$} if $f \circ \gamma \in RS([a, b], \gamma; E)$. In which case, 
+    \[
+    \int_\gamma f = \int_a^b f(\gamma(t)) \gamma(dt)
+    \]
+
+    is the \textbf{path integral} of $f$ with respect to $\gamma$. The set $PI([a, b], \gamma; E)$ is the space of all functions path-integrable with respect to $\gamma$. 
+\end{definition}
+
+\begin{proposition}[Change of Variables]
+\label{proposition:path-integral-change-of-variables}
+    Let $[a, b], [c, d] \subset \real$, $E, F, H$ be locally convex spaces over $K \in \RC$, $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous bilinear map, $\gamma \in C([a, b]; F)$ be a path, and $\varphi: C([c, d]; [a, b])$ be non-decreasing with $\varphi(c) = a$ and $\varphi(d) = b$, then for any $f \in PI([a, b], \gamma; E)$, $f \in PI([c, d], \gamma \circ \varphi; E)$, and
+    \[
+    \int_\gamma f = \int_{\gamma \circ \varphi} f
+    \]
+\end{proposition}
+\begin{proof}
+    Since $\varphi(c) = a$, $\varphi(d) = b$, and $\varphi$ is continuous, it is surjective. As $\varphi$ is also non-decreasing, for any tagged partition $(P = \seqfz{x_j}, c = \seqf{c_j}) \in \scp_t([a, b])$, there exists a tagged partition $(Q = \seqfz{y_j}, d = \seqf{d_j}) \in \scp_t([c, d])$ such that $\varphi(y_j) = x_j$ for each $0 \le j \le n$ and $\varphi(d_j) = c_j$ for each $1 \le j \le n$. In addition,  
+    \begin{align*}
+        S(P, c, f \circ \gamma, \gamma) &= \sum_{j = 1}^n f \circ \gamma(c_j)[\gamma(x_j) - \gamma(x_{j - 1})] \\
+        &= \sum_{j = 1}^n f \circ \gamma \circ \varphi (d_j)[\gamma \circ \varphi(y_j) - \gamma \circ \varphi(y_{j-1})] \\
+        &= S(Q, d, f \circ \gamma \circ \varphi, \gamma \circ \varphi)
+    \end{align*}
+
+    Therefore if $f \in PI([a, b], \gamma; E)$, then $f \in PI([c, d], \gamma \circ \varphi; E)$, with $\int_\gamma f = \int_{\gamma \circ \varphi} f$.
+\end{proof}
+
+\begin{definition}[Curve]
+\label{definition:rs-curve}
+    Let $[a, b], [c, d] \subset \real$, $F$ be a locally convex space over $K \in \RC$, and $\gamma \in C([a, b]; F)$ and $\mu \in C([c, d]; F)$ be paths, then $\gamma$ and $\mu$ are \textbf{equivalent} if there exists a continuous, strictly increasing bijection $\varphi \in C([c, d]; [a, b])$ such that $\mu = \gamma \circ \varphi$. In which case, $\varphi$ is a \textbf{change of parameter} between $\gamma$ and $\mu$. 
+
+    A \textbf{curve} in $F$ is then an equivalence class of paths. 
+\end{definition}
+
+\begin{lemma}
+\label{lemma:rectifiable-piecewise-linear}
+    Let $[a, b] \subset \real$, $E, F, H$ be locally convex spaces over $K \in \RC$, $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous bilinear map, $\gamma \in C([a, b]; F)$ be a rectifiable path, and $U \in \cn_F(\gamma([a, b]))$, then for any continuous seminorm $[\cdot]_G: G \to [0, \infty)$, $\eps > 0$, and $f \in C(U; E)$, there exists a piecewise linear path $\Gamma \in C([a, b]; F)$ such that:
+    \begin{enumerate}
+        \item $\Gamma(a) = \gamma(a)$ and $\Gamma(b) = \gamma(b)$. 
+        \item $\braks{\int_\gamma f - \int_\Gamma f}_F < \epsilon$. 
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    Let $[\cdot]_E: E \to [0, \infty)$ and $[\cdot]_F: F \to [0, \infty)$ such that for any $x \in E$ and $y \in F$, $[xy]_G \le [x]_E[y]_F$. Since $\gamma([a, b])$ is compact, by modifying $[\cdot]_F$, assume without loss of generality that there exists $V \in \cn_F(\gamma([a, b]))$ such that for any $x, y \in V$ with $[x - y]_F \le 1$, $[f(x) - f(y)]_E \le \eps$.
+
+    Since $f \in C(U; E)$, $f \in PI([a, b], \gamma; E)$ by \autoref{proposition:rs-bv-continuous}. Given that $\gamma$ is of bounded variation, there exists $(P  = \seqfz{x_j}, c) \in \scp_t([a, b])$ such that:
+    \begin{enumerate}[label=(\alph*)]
+        \item For each $1 \le j \le n$, 
+        \[
+        \gamma([x_{j-1}, x_j]) \subset \bracs{y \in F|[y - x_{j-1}]_F \le 1}
+        \]
+        \item $\braks{\int_\gamma f - S(P, c, f \circ \gamma, \gamma)}_G < \epsilon$.
+    \end{enumerate}
+
+    Let $\Gamma$ be the piecewise linear path formed by linearing $f$ at points in $P$. For any $(Q, d) \in \scp_t([a, b])$ with $(Q, d) \ge (P, c)$, 
+    \[
+    \braks{S(P, c, f \circ \gamma, \gamma) - S(Q, d, f \circ \Gamma, \Gamma)}_G \le \eps [\gamma]_{\text{var}, [\cdot]_F}
+    \]
+
+    As $\Gamma$ is also of bounded variation, $f \in PI([a, b], \Gamma; E)$. Since the above holds for all refinements of $(Q, d)$, 
+    \[
+    \braks{\int_\gamma f - \int_\Gamma f}_G < \eps(1 + [\gamma]_{\text{var}, [\cdot]_F})
+    \]
+
+    
+\end{proof}
+
+
+\begin{theorem}[Fundamental Theorem of Calculus for Path Integrals]
+\label{theorem:ftc-path-integrals}
+    Let $[a, b], [c, d] \subset \real$, $E, F$ be separated locally convex spaces, $\gamma \in C([a, b]; F)$ be a rectifiable path, $U \in \cn_F(\gamma([a, b]))$.
+    
+    Let $\sigma \subset \mathfrak{B}(F)$ be an ideal containing all compact sets, then for any $f \in C^1_\sigma(U; E)$, 
+    \[
+    \int_\gamma D_\sigma f = f(\gamma(b)) - f(\gamma(a))
+    \]
+\end{theorem}
+\begin{proof}
+    Using \autoref{lemma:rectifiable-piecewise-linear}, assume without loss of generality that $\gamma$ is piecewise smooth. By the \hyperref[Chain Rule]{proposition:chain-rule-sets}, $f \circ \gamma \in C^1([a, b]; F)$ with $D(f \circ \gamma)(t) = Df(\gamma(t)) \cdot D\gamma(t)$. In which case, by \autoref{proposition:lebesgue-stieltjes-differentiable} and the \hyperref[Fundamental Theorem of Calculus]{theorem:ftc-riemann},
+    \begin{align*}
+    \int_\gamma D_\sigma f &= \int_a^b D_\sigma f (\gamma(t)) \cdot D\gamma(t)dt \\
+    &= \int_a^b D(f \circ \gamma)(t) dt =  f(\gamma(b)) - f(\gamma(a))
+    \end{align*}
+\end{proof}
+
+
+
+
+
+

src/fa/rs/rs-bv.tex

@@ -1,9 +1,9 @@
-\section{Riemann-Stieltjes Integrals and Functions of Bounded Variation}
+\section{Integrators of Bounded Variation}
 \label{section:rs-bv}
 
 \begin{proposition}
 \label{proposition:rs-bound}
-    Let $[a, b] \subset \real$, $E, F, H$ be locally convex spaces, and $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous bilinear map, and $G: [a, b] \to F$.
+    Let $[a, b] \subset \real$, $E, F, H$ be locally convex spaces, $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous bilinear map, and $G: [a, b] \to F$.
 
     Let $[\cdot]_H$ be a continuous seminorm on $H$, then there exists continuous seminorms $[\cdot]_E$ on $E$ and $[\cdot]_F$ on $F$ such that for any $f \in RS([a, b], G)$,
     \[
@@ -24,7 +24,7 @@
 
 \begin{proposition}
 \label{proposition:rs-complete}
-    Let $[a, b] \subset \real$, $E, F, H$ be locally convex spaces, and $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous bilinear map, and $G \in BV([a, b]; F)$.
+    Let $[a, b] \subset \real$, $E, F, H$ be locally convex spaces, $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous bilinear map, and $G \in BV([a, b]; F)$.
 
     For each continuous seminorm $\rho$ on $E$ and $f: [a, b] \to E$, define
     \[