Added the homotopic version of Cauchy's theorem.

src/fa/rs/path.tex

@@ -43,16 +43,18 @@
 
 \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) \cap PI([a, b], \gamma; E)$, there exists a piecewise linear path $\Gamma \in C([a, b]; F)$ such that:
+    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]))$.
+    
+    For each $P \in \scp([a, b])$, let $\Gamma_P \in C([a, b]; F)$ be the piecewise linear path obtained by interpolating values of $\gamma$ at points of $P$, then for any continuous seminorm $[\cdot]_G: G \to [0, \infty)$, $\eps > 0$, and $f \in C(U; E) \cap PI([a, b], \gamma; E)$, there exists $P \in \scp([a, b])$ such that for any $Q \in \scp([a, b])$ with $Q \ge P$,
     \begin{enumerate}
-        \item $\Gamma(a) = \gamma(a)$ and $\Gamma(b) = \gamma(b)$. 
-        \item $\braks{\int_\gamma f - \int_\Gamma f}_F < \epsilon$. 
+        \item $\Gamma_P(a) = \gamma(a)$ and $\Gamma_P(b) = \gamma(b)$. 
+        \item $\braks{\int_\gamma f - \int_{\Gamma_P} 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 continuous, 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_0, c_0) \in \scp_t([a, b])$ such that for any $(P = \seqfz{x_j}, c) \in \scp_t([a, b])$ with
     \begin{enumerate}[label=(\alph*)]
         \item For each $1 \le j \le n$, 
         \[
@@ -61,7 +63,7 @@
         \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)$, 
+    Let $\Gamma = \Gamma_P$, then 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}
     \]
@@ -70,8 +72,6 @@
     \[
     \braks{\int_\gamma f - \int_\Gamma f}_G < \eps(1 + [\gamma]_{\text{var}, [\cdot]_F})
     \]
-
-    
 \end{proof}
 
 \begin{remark}
@@ -81,7 +81,7 @@
 
 \begin{lemma}
 \label{lemma:rectifiable-smooth}
-    Let $[a, b] \subset \real$, $E, F, H$ be separated locally convex spaces over $K \in \RC$ with $H$ being complete, $E \times F \to H$ with $(x, y) \mapsto xy$ be a continuous bilinear map, $\gamma \in C([a, b]; F)$ be a piecewise linear path, and $U \in \cn_F(\gamma([a, b]))$. 
+    Let $[a, b] \subset \real$, $E$ be a separated locally convex space over $K \in \RC$, $F$ be a Banach space over $K$, $H$ be a complete locally convex space over $K$, all 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 piecewise $C^1$ curve that is constant on $[a, a + \eps)$ and $(b - \eps, b]$, and $U \in \cn_F(\gamma([a, b]))$. 
 
     Extend $\gamma$ to $\real$ by 
     \[
@@ -92,7 +92,7 @@
     \end{cases}
     \]
 
-    Since $\gamma$ takes values in a finite-dimensional subspace, assume without loss of generality that $F$ is a Banach space. In which case, for each $\varphi \in C_c^\infty(\real; \real)$ with $\int_\real \varphi = 1$ and $t > 0$, let
+    For each $\varphi \in C_c^\infty(\real; \real)$ with $\int_\real \varphi = 1$ and $t > 0$, let
     \[
     \gamma_t: [a, b] \to F \quad x \mapsto \frac{1}{t}\int_{\real} \ol \gamma(y) \varphi\braks{\frac{x - y}{t}} dy
     \]
@@ -109,8 +109,6 @@
     \end{enumerate}
 \end{lemma}
 \begin{proof}
-    By passing through a \hyperref[reparametrisation]{proposition:path-integral-change-of-variables}, assume without loss of generality that there exists $\eps > 0$ such that $\gamma$ is constant on $[a, a + \eps)$ and $(b - \eps, b]$. 
-
     (1): By the \hyperref[Mean Value Theorem]{theorem:mean-value-theorem}, for each $x, y \in [a, b]$, 
     \[
     \norm{\frac{\varphi(x) - \varphi(y)}{x - y}}_F \le \sup_{z \in \real}\norm{D\varphi(z)}_F