Fixed mistakes in FTC for path integrals.

src/fa/rs/path.tex

@@ -52,7 +52,7 @@
 \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:
+    Since $f \in C(U; E)$, $f \in PI([a, b], \gamma; E)$ by \autoref{proposition:rs-bv-continuous}. Given that $\gamma$ is continuous, 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$, 
         \[
@@ -74,12 +74,16 @@
     
 \end{proof}
 
+\begin{remark}
+\label{remark:piecewise-linear-remark}
+    Past me made the mistake of believing that in \autoref{lemma:rectifiable-piecewise-linear}, it is possible to approximate rectifiable curves with piecewise linear curves in \textit{total variation distance}. However, this is not possible: as every piecewise linear curve is absolutely continuous, and the limit of these curves in total variation distance must also be absolutely continuous. As such, this strong approximation exists if and only if the curve is absolutely continuous. 
+\end{remark}
+
+
 
 \begin{theorem}[Fundamental Theorem of Calculus for Path Integrals]
 \label{theorem:ftc-path-integrals}
-    Let $[a, b] \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)$, 
+    Let $[a, b] \subset \real$, $E, F$ be separated locally convex spaces, $\sigma \subset \mathfrak{B}(F)$ be an ideal containing all compact sets, $\gamma \in C([a, b]; F)$ be a rectifiable path, and $U \in \cn_F(\gamma([a, b]))$, then for any $f \in C^1_\sigma(U; E)$, 
     \[
     \int_\gamma D_\sigma f = f(\gamma(b)) - f(\gamma(a))
     \]
@@ -87,7 +91,7 @@
     In particular, if $\gamma(a) = \gamma(b)$, then $\int_\gamma D_\sigma f = 0$. 
 \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},
+    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-conditions}, $f \circ \gamma$ is piecewise $C^1$ with $D(f \circ \gamma)(t) = Df(\gamma(t)) \cdot D\gamma(t)$ on all but finitely many points. In which case, by \hyperref[change of variables formula]{theorem:rs-change-of-variables} 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))

src/fa/rs/regulated.tex

@@ -4,7 +4,7 @@
 
 \begin{proposition}
 \label{proposition:rs-interval}
-    Let $[a, b] \subset \real$, $E, F, H$ be TVSs over $K \in \RC$, and $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous linear map. 
+    Let $[a, b] \subset \real$, $E, F, H$ be TVSs over $K \in \RC$, and $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous bilinear map. 
     
     Let $G: [a, b] \to F$ and $[c, d] \subset [a, b]$ such that $G$ is continuous at $c$ and $d$, then for any $x \in E$, $x \cdot \one_{[c, d]} \in RS([a, b], G)$, and
     \[
@@ -35,9 +35,9 @@
 
 \begin{definition}[Regulated Function]
 \label{definition:regulated-function}
-    Let $[a, b] \subset \real$, $E, F, H$ be TVSs over $K \in \RC$, and $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous linear map. 
+    Let $[a, b] \subset \real$, $E, F, H$ be TVSs over $K \in \RC$, and $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous bilinear map. 
 
-    Let $G: [a, b] \to F$ and $f: [a, b] \to E$ be a step map, then $f$ is \textbf{regulated with respect to} $G$ if $G$ is continuous on all discontinuity points of $f$. Let $\text{Reg}([a, b], G; E)$ be closure of all regulated step maps with respect to the uniform norm, then:
+    Let $G: [a, b] \to F$ and $f: [a, b] \to E$ be a step map, then $f$ is \textbf{regulated with respect to} $G$ if $G$ is continuous on all discontinuity points of $f$. Let $\text{Reg}([a, b], G; E)$ be closure of all regulated step maps with respect to the uniform topology, then:
     \begin{enumerate}
         \item Every regulated step map is in $RS([a, b], G)$. 
         \item If $E$ is metrisable, then for any $f \in \text{Reg}([a, b], G; E)$, $f$ is continuous at all but at most countably many points, and $f$ does not share any discontinuity points with $E$. 
@@ -106,4 +106,3 @@
     (2): Let $G(x) = \int_a^x DF(t)dt + F(a)$, then $G - F$ has derivative $0$. By the \hyperref[Mean Value Theorem]{proposition:zero-derivative-constant}, $G - F$ is constant. As $G(a) - F(a) = 0$, $G  = F$. 
     
 \end{proof}
-

src/fa/rs/rs.tex

@@ -76,3 +76,30 @@
 \end{proof}
 
 
+
+\begin{theorem}[Change of Variables]
+\label{theorem:rs-change-of-variables}
+    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 $G \in C^1([a, b]; F)$, then for any bounded $f \in RS([a, b], G; E)$, 
+    \[
+    \int_a^b f(t) G(dt) = \int_a^b f(t) DG(t) dt
+    \]
+\end{theorem}
+\begin{proof}
+    Let $[\cdot]_H: H \to [0, \infty)$ be a continuous seminorm and $[\cdot]_E: E \to [0, \infty)$ and $[\cdot]_F: F \to [0, \infty)$ be continuous seminorms on $E$ and $F$, respectively, such that for any $x \in E$ and $y \in F$, $[xy]_H \le [x]_E[y]_F$. 
+
+    Since $G \in C^1([a, b]; F)$, $DG \in UC([a, b]; F)$ by \autoref{proposition:uniform-continuous-compact}. Thus there exists $\delta > 0$ such that $[DG(x) - DG(y)]_F < \eps$ for all $x, y \in [a, b]$ with $|x - y| \le \delta$. Let $(P = \seqfz{x_j}, c = \seqf{c_j}) \in \scp_t([a, b])$ with $\sigma(P) \le \delta$, then by the \hyperref[Mean Value Theorem]{theorem:mean-value-theorem-line}, for each $1 \le j \le n$, 
+    \begin{align*}
+        &G(x_j) - G(x_{j-1}) - (x_j - x_{j-1})DG(c_j) \\
+        &\in (x_j - x_{j-1})\ol{\text{Conv}}\bracs{DG(t) - DG(c_j)|t \in [x_{j-1}, x_j]}
+    \end{align*}
+
+    so
+    \[
+    [G(x_j) - G(x_{j-1}) - (x_j - x_{j-1})DG(c_j)]_F \le \eps(x_j - x_{j-1})
+    \]
+
+    and
+    \[
+        [S(P, c, f, G) - S(P, c, f \cdot DG, \text{Id})]_H \le \eps \cdot (b - a) \cdot \sup_{x \in [a, b]}[f(x)]_E
+    \]
+\end{proof}