From 02bd8479bce14f6e94aca0122b7fac74a0a601ce Mon Sep 17 00:00:00 2001 From: Bokuan Li Date: Wed, 27 May 2026 22:59:06 -0400 Subject: [PATCH] Added path lemma. --- .vscode/settings.json | 4 +++ .vscode/tasks.json | 2 +- src/dg/complex/derivative.tex | 58 +++++++++++++++++++++++++++++++++++ src/dg/complex/space.tex | 12 ++++++++ src/fa/lc/convex.tex | 6 +++- src/fa/lc/inductive.tex | 13 ++++++++ 6 files changed, 93 insertions(+), 2 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index 469687c..2ffa357 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -7,6 +7,10 @@ { "label": "Conservative Watch", "task": "Conservative" + }, + { + "label": "Compile All", + "task": "Build" } ], "latex.linting.enabled": false, diff --git a/.vscode/tasks.json b/.vscode/tasks.json index 74c83ef..803e9e4 100644 --- a/.vscode/tasks.json +++ b/.vscode/tasks.json @@ -4,7 +4,7 @@ { "label": "Build", "type": "shell", - "command": "npx spec compile", + "command": "npx spec compile --all", "windows": { "options": { "shell": { diff --git a/src/dg/complex/derivative.tex b/src/dg/complex/derivative.tex index c55f730..ab89dbd 100644 --- a/src/dg/complex/derivative.tex +++ b/src/dg/complex/derivative.tex @@ -280,5 +280,63 @@ (5) $\Rightarrow$ (3): By the equivalence of the prior points, for any $\phi \in E^*$, $\phi \circ f$ satisfies (3). By the \hyperref[Hahn-Banach Theorem]{proposition:hahn-banach-utility}, $f$ also satisfies (3). \end{proof} +\begin{proposition} +\label{proposition:existence-curves} + Let $K \subset \complex$ be compact and $U \in \cn_\complex(K)$, then there exists closed rectifiable curves $\seqf{\gamma_j}$ such that for any separated locally convex space $E$, $f \in H(U; E)$, and $z_0 \in K$, + \[ + f(z) = \sum_{j = 1}^n \int_{\gamma_j} \frac{f(z)}{z - z_0}dz + \] +\end{proposition} +\begin{proof}[Proof, {{\cite[Proposition VIII.1.1]{ConwayComplex}}}. ] + Via \hyperref[fattening]{proposition:distance-compact}, let $V \in \cn_\complex^o(K)$ precompact with $\ol V \subset U$. Identify $\complex = \real^2$, then since $V$ is precompact, there exists $\delta > 0$ and $\seqf{(x_j, y_j)} \subset U$ such that: + \begin{enumerate} + \item For each $1 \le j \le n$, $R_j = [x_j, x_j + \delta] \times [y_j, y_j + \delta] \subset U$. + \item $\bigcup_{j = 1}^n R_j \supset V$. + \item $x_j, y_j = 0 \mod \delta$. + \end{enumerate} + + In other words, $V$ is covered with a grid of squares with side-length $\delta$ and corners $\seqf{(x_j, y_j)}$. Now, for each $1 \le j \le n$ and $t \in [0, 1]$, let + \begin{align*} + \gamma_{j, \rightarrow}(t) &= (1 - t)(x_j, y_j) + t(x_j + \delta, y_j) \\ + \gamma_{j, \uparrow}(t) &= (1 - t)(x_j + \delta, y_j) + t(x_j + \delta, y_j + \delta) \\ + \gamma_{j, \leftarrow}(t) &= (1 - t)(x_j + \delta, y_j + \delta) + t(x_j, y_j + \delta) \\ + \gamma_{j, \downarrow}(t) &= (1 - t)(x_j, y_j + \delta) + t(x_j, y_j) \\ + \end{align*} + + and $\gamma_j = \gamma_{j, \downarrow} \cdot \gamma_{j, \leftarrow} \cdot \gamma_{j, \uparrow} \cdot \gamma_{j, \rightarrow}$ be their concatenation, then for each $z \in U \setminus \partial R_j$, + \[ + \int_{\gamma_j} \frac{f(z)}{z - z_0}dz = \begin{cases} + f(z) &z \in R_j^o \\ + 0 &z \in U \setminus R_j + \end{cases} + \] + + by \hyperref[Cauchy's Integral Formula]{theorem:cauchy-formula}. Let $\seqf[N]{\mu_j}$ be an enumeration of + \[ + \bigcup_{j = 1}^n \bracs{\gamma_{j, \downarrow}, \gamma_{j, \leftarrow}, \gamma_{j, \uparrow}, \gamma_{j, \rightarrow}} + \] + + then for each $z_0 \in \bigcup_{j = 1}^n R_j^o$ and $f \in H(U; E)$, + \[ + f(z) = \sum_{j = 1}^N \int_{\mu_j}\frac{f(z)}{z - z_0}dz + \] + + From here, it is sufficient to eliminate line segments that intersect $K$ and ensure that the remaining segments form a collection of loops. Let $1 \le j \le k \le N$, then $(\mu_j, \mu_k)$ is \textit{redundant} if for each $t \in [0, 1]$, $\mu_j(t) = \mu_k(1 - t)$. If $(\mu_j, \mu_k)$ are redundant, then + \begin{enumerate}[start=3] + \item There exists no $1 \le l \le N$ with $l \ne j, k$ such that $(\mu_j, \mu_l)$ or $(\mu_k, \mu_l)$ is redundant. + \item $\int_{\mu_j}\frac{f(z)}{z - z_0}dz + \int_{\mu_k}\frac{f(z)}{z - z_0}dz = 0$. + \end{enumerate} + + so every line segment either cannot form a redundant pair, or forms a unique one. + + By relabeling, let $\bracs{\mu_j|1 \le j \le m}$ such that for each $1 \le j \le m$, there exists no $1 \le k \le n$ such that $(\mu_j, \mu_k)$ is redundant. By (5), for each $z_0 \in \bigcup_{j = 1}^n R_j^o$ and $f \in H(U; E)$, + \[ + f(z) = \sum_{j = 1}^m \int_{\mu_j}\frac{f(z)}{z - z_0}dz + \] + + Let $1 \le j \le N$ such that $\mu_j([0, 1]) \cap K \ne \emptyset$. Since $V \in \cn_\complex(K)$, there exists $1 \le k \le N$ such that $(\mu_j, \mu_k)$ are redundant by (2) and (3). Therefore $\bigcup_{j = 1}^m \mu_j([0, 1]) \cap K = \emptyset$. Since $\bigcup_{j = 1}^n R_j^o$ is dense in $K$, the above also holds for all $z \in K$. + + Finally, let $1 \le j \le m$. Since $\mu_j$ does not form a redundant pair, $\mu_j(1)$ intersects at most two distinct squares by (3). In which case, there must exist $1 \le k \le m$ such that $\mu_k(0) = \mu_j(1)$. Therefore $\seqf[m]{\mu_j}$ forms a collection of closed rectifiable curves. +\end{proof} diff --git a/src/dg/complex/space.tex b/src/dg/complex/space.tex index ed88fee..d60fb53 100644 --- a/src/dg/complex/space.tex +++ b/src/dg/complex/space.tex @@ -38,3 +38,15 @@ (C1) $\Leftrightarrow$ (C2): By the \hyperref[Arzelà-Ascoli Theorem]{theorem:arzela-ascoli}. \end{proof} + +\begin{definition}[Space of Holomorphic Functions Near a Set] +\label{definition:holomorphic-function-space-near} + Let $E$ be a complete separated locally convex space over $\complex$ and $A \subset \complex$. Direct $\cn_{\complex}^o(A)$ under reverse inclusion, then the inductive limit + \[ + H(A; E) = \varinjlim_{U \in \cn_{\complex}^o(A)} H(U; E) + \] + + is the \textbf{space of holomorphic functions near} $A$, and is of type (LF). +\end{definition} + + diff --git a/src/fa/lc/convex.tex b/src/fa/lc/convex.tex index af08b9d..cb29764 100644 --- a/src/fa/lc/convex.tex +++ b/src/fa/lc/convex.tex @@ -186,7 +186,7 @@ \begin{definition}[Locally Convex Space] \label{definition:locally-convex} - Let $E$ be a TVS over $\RC$, then the following are equivalent: + Let $E$ be a TVS over $K \in \RC$, then the following are equivalent: \begin{enumerate} \item There exists a fundamental system of neighborhoods at $0$ consisting of convex sets. \item There exists a fundamental system of neighbourhoods at $0$ consisting of convex, circled, and radial sets. @@ -203,6 +203,10 @@ $(3) \Rightarrow (1)$: For each $i \in I$ and $r > 0$, $\bracs{x \in E| [x]_i < r}$ is convex. \end{proof} +\begin{definition}[Fréchet Space] +\label{definition:frechet-space} + Let $E$ be a locally convex space over $K \in \RC$, then $E$ is a \textbf{Fréchet space} if $E$ is first countable and complete. +\end{definition} \begin{definition}[Associated Normed Space] diff --git a/src/fa/lc/inductive.tex b/src/fa/lc/inductive.tex index 825bc83..e31dd4b 100644 --- a/src/fa/lc/inductive.tex +++ b/src/fa/lc/inductive.tex @@ -268,3 +268,16 @@ which contradicts the fact that $(F_n + U) \cap E_n = \emptyset$. \end{proof} + +\begin{definition}[Space of Type (LB)] +\label{definition:lb-space} + Let $E$ be a locally convex space, then $E$ is of type \textbf{(LB)} if $E$ is the strict inductive limit of a countable system of Banach spaces. +\end{definition} + +\begin{definition}[Space of Type (LF)] +\label{definition:lf-space} + Let $E$ be a locally convex space, then $E$ is of type \textbf{(LF)} if $E$ is the strict inductive limit of a countable system of Fréchet spaces. +\end{definition} + + +