From af1fa616680b06fffdb2593570c8478ad9debcfc Mon Sep 17 00:00:00 2001 From: Bokuan Li Date: Sun, 22 Mar 2026 17:12:22 -0400 Subject: [PATCH] Added the fundamental theorem of calculus. --- src/fa/rs/bv.tex | 58 ++++++++++++++++++-- src/fa/rs/index.tex | 2 + src/fa/rs/regulated.tex | 109 ++++++++++++++++++++++++++++++++++++++ src/fa/rs/rs-measure.tex | 91 +++++++++++++++++++++++++++---- src/fa/rs/rs.tex | 24 --------- src/topology/main/lch.tex | 2 +- 6 files changed, 246 insertions(+), 40 deletions(-) create mode 100644 src/fa/rs/regulated.tex diff --git a/src/fa/rs/bv.tex b/src/fa/rs/bv.tex index e63f94f..4ec07e8 100644 --- a/src/fa/rs/bv.tex +++ b/src/fa/rs/bv.tex @@ -6,7 +6,7 @@ \label{definition:total-variation} Let $E$ be a locally convex space, $\rho$ be a continuous seminorm on $E$, $f: [a, b] \to E$, and $P \in \scp([a, b])$ be a partition, then \[ - V_{\rho, p}(f) = \sum_{j = 1}^n \rho(f(x_j) - f(x_{j - 1})) + V_{\rho, P}(f) = \sum_{j = 1}^n \rho(f(x_j) - f(x_{j - 1})) \] is the \textbf{variation} of $f$ with respect to $\rho$ and $P$. The supremum over all such partitions @@ -19,7 +19,45 @@ If $E$ is a normed vector space, then the variation and total variation of $f$ is taken with respect to its norm. \end{definition} -\begin{definition}[Bounded Variation, {{\cite[Proposition X.1.1]{Lang}}}] +\begin{definition}[Variation Function] +\label{definition:variation-function} + Let $E$ be a locally convex space, $\rho$ be a continuous seminorm on $E$, $f: [a, b] \to E$, then the function + \[ + T_{f, \rho}(x) = \sup_{P \in \scp([a, x])}V_{\rho, P}(f) = [f|_{[a, x]}]_{\text{var}, \rho} + \] + + is the \textbf{variation function} of $f$ with respect to $\rho$, and: + \begin{enumerate} + \item $T_{f, \rho}: [a, b] \to [0, \infty]$ is a non-negative, non-decreasing function. + \item If $f \in BV([a, b]; E)$, then for any $[c, d] \subset [a, b]$, $[f]_{\text{var}, \rho} = T_{f, \rho}(d) - T_{f, \rho}(a)$. + \end{enumerate} +\end{definition} +\begin{proof} + (2): Let $P \in \scp([a, c])$ and $Q = \seqf{x_j} \in \scp([a, d])$ be partitions containing $P$, then + \[ + V_{\rho, Q}(f) - V_{\rho, P}(f) = \sum_{x_j > c}\rho(f(x_j) - f(x_{j - 1})) \le [f]_{\text{var}, \rho} + \] + + As this holds for all $Q \in \scp([a, d])$ containing $P$, + \[ + T_{f, \rho}(d) - T_{f, \rho}(c) \le T_{f, \rho}(d) - V_{\rho, P}(f) \le [f|_{[c, d]}]_{\text{var}, \rho} + \] + + On the other hand, for any $R \in \scp([c, d])$, $P \cup R \in \scp([a, d])$ and contains $P$. Therefore + \[ + T_{f, \rho}(d) - V_{\rho, P}(f) \ge V_{\rho, R \cup P}(f) - V_{\rho, P}(f) = V_{\rho, R}(f) + \] + + Since this holds for all $P \in \scp([a, c])$, + \[ + T_{f, \rho}(d) - T_{f, \rho}(c) \ge V_{\rho, R}(f) + \] + + and as the above holds for all $R \in \scp([c, d])$, $T_{f, \rho}(d) - T_{f, \rho}(c) \ge [f|_{[c, d]}]_{\text{var}, \rho}$. +\end{proof} + + +\begin{definition}[Bounded Variation] \label{definition:bounded-variation} Let $E$ be a locally convex space, $\rho$ be a continuous seminorm on $E$, and $f: [a, b] \to E$. If $[f]_{\text{var}, \rho} < \infty$, then $f$ is of \textbf{bounded variation} with respect to $\rho$. @@ -40,7 +78,7 @@ \item[(5)] $f$ has at most countably many discontinuities. \end{enumerate} \end{definition} -\begin{proof} +\begin{proof}[Proof {{\cite[Proposition X.1.1]{Lang}}}. ] (3): Let $\rho$ be a continuous seminorm on $E$ and $P \in \scp([a, b])$, then by assumption (a), \[ V_{\rho, P}(f) = \sum_{j = 1}^n \rho(f(x_j) - f(x_{j - 1})) @@ -71,7 +109,19 @@ \begin{proposition} \label{proposition:bounded-variation-one-side-limit} - + Let $E$ be a complete locally convex space and $f \in BV([a, b]; E)$, then for each $x \in [a, b]$, the limits $\lim_{y \downto x}f(y)$ and $\lim_{y \upto x}f(y)$ exist. \end{proposition} +\begin{proof} + By flipping $f$, it is sufficient to consider the right-side limit $\lim_{y \downto x}f(y)$. + + Let $\rho: E \to [0, \infty)$ be a continuous seminorm on $E$, and $T_{\rho, f}: [a, b] \to [0, \infty)$ be the variation function of $f$ with respect to $\rho$. For any $\eps > 0$, there exists $\delta > 0$ such that $T_{\rho, f}(z) - \lim_{y \downto x}T_{\rho, f}(y) < \eps$ for all $z \in (x, x + \delta)$. In which case, for any $x < y < z < x + \delta$, + \[ + \rho(f(z) - f(y)) \le [f|_{y, z}]_{\text{var}, \rho} \le T_{\rho, f}(z) - T_{\rho, f}(y) \le T_{\rho, f}(z) - \lim_{u \downto x}T_{\rho, f}(u) < \eps + \] + + By completeness of $E$, the limit $\lim_{y \downto x}f(y)$ exists. +\end{proof} + + diff --git a/src/fa/rs/index.tex b/src/fa/rs/index.tex index 06e69b1..2999274 100644 --- a/src/fa/rs/index.tex +++ b/src/fa/rs/index.tex @@ -5,3 +5,5 @@ \input{./bv.tex} \input{./rs.tex} \input{./rs-bv.tex} +\input{./regulated.tex} +\input{./rs-measure.tex} diff --git a/src/fa/rs/regulated.tex b/src/fa/rs/regulated.tex new file mode 100644 index 0000000..6f1bd2a --- /dev/null +++ b/src/fa/rs/regulated.tex @@ -0,0 +1,109 @@ +\section{Regulated Functions} +\label{section:regulated-function} + + +\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 $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 + \[ + \int_a^b x \cdot \one_{[c, d]} dG = x \cdot [G(d) - G(c)] + \] +\end{proposition} +\begin{proof} + Assume without loss of generality that $a < c \le d < b$. Let $U \in \cn_H(0)$, then there exists $V \in \cn_F(0)$ such that $xV \subset U$. By continuity of $G$, there exists $\delta > 0$ such that $G((c - \delta, c]) - G(c) \subset V$ and $G([d, d + \delta)) - G(d) \subset V$. In which case, for any tagged partition $(P = \bracsn{x_j}_0^n, t = \seqf{t_j})$ that contains $\bracs{c - \delta, c, d, d + \delta}$, + \begin{align*} + S(Q, t, x \cdot \one_{[c, d]}, G) &= x\sum_{a < x_j \le c - \delta}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\ + &+ x \sum_{c - \delta < x_j \le c}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\ + &+ x \sum_{c < x_j \le d}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j-1})] \\ + &+ x \sum_{d < x_j \le d + \delta}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\ + &+ x \sum_{d + \delta < x_j \le b}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\ + &= x \sum_{c - \delta \le x_j \le c}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\ + &+ x \cdot [G(d) - G(c)] \\ + &+ x \sum_{d < x_j \le d + \delta}\one_{[c, d]}[G(x_j) - G(x_{j - 1})] \\ + &\in G(d) - G(c) + xG([c - \delta, c]) + xG([d, d + \delta]) \\ + &\subset x \cdot [G(d) - G(c)] + xV + xV \subset [G(d) - G(c)] + U + U + \end{align*} +\end{proof} + + +\begin{definition}[Step Map] +\label{definition:step-map} + Let $[a, b] \subset \real$, $E$ be a TVS, $f: [a, b] \to E$ be a function, and $P = \bracsn{x_j}_1^n \in \scp([a, b])$, then $f$ is a \textbf{step map} with respect to $P$ if for each $1 \le j \le n$, $f$ is constant on $(x_{j - 1}, x_j)$. +\end{definition} + +\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 $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 $f$ is continuous on all discontinuity points of $G$. Let $\text{Reg}([a, b], G; E)$ be closure of all regulated step maps with respect to the uniform norm, 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$. + \item If $E, F, H$ are locally convex, $G \in BV([a, b]; F)$, and $H$ is complete, then $\text{Reg}([a, b], G; E) \subset RS([a, b], G)$. + \item If $F$ is normed and $G \in BV([a, b]; F)$, then $\text{Reg}([a, b], G; E) \supset C([a, b]; E)$. + \end{enumerate} + + The set $\text{Reg}([a, b], G; E)$ is the space of \textbf{regulated functions} with respect to $G$. If $G = \text{Id}$, then $\text{Reg}([a, b]; E) = \text{Reg}([a, b], G; E)$ denotes the space of regulated functions on $[a, b]$. +\end{definition} +\begin{proof} + (1): If $f: [a, b] \to E$ is a regulated step map, then there exists $\seqf{[a_j, b_j]} \subset 2^{[a, b]}$ and $\seqf{x_j}$ such that + \begin{enumerate} + \item $f = \sum_{j = 1}^n x_j \one_{[a_j, b_j]}$. + \item For each $1 \le j \le n$, $G$ is continuous at $a_j$ and $b_j$. + \end{enumerate} + + Thus $f \in RS([a, b], G)$ by \autoref{proposition:rs-interval}. + + (2): Let $f \in \text{Reg}([a, b], G; E)$, then there exists regulated step maps $\seq{f_n} \subset \text{Reg}([a, b], G; E)$ such that $f_n \to f$ uniformly. For each $n \in \natp$, let $D_n$ be the set of discontinuity points of $f_n$. Let $x \in [a, b] \setminus \bigcup_{n \in \natp}D_n$. For any symmetric neighbourhood $U \in \cn_E(0)$, there exists $n \in \natp$ such that $(f_n - f)([a, b]) \subset U$. Since $f_n$ is continuous at $x$, there exists $\eps > 0$ such that $f_n((x - \eps, x + \eps)) - f_n(x) \in U$. In which case, + \begin{align*} + f((x - \eps, x + \eps)) - f(x) &\subset (f_n - f)((x - \eps, x + \eps)) + (f_n - f)(x) \\ + &+ f_n((x - \eps, x + \eps)) - f_n(x) \\ + &\subset U + U + U + \end{align*} + + Therefore $f$ is continuous at $x$. Since each $D_n$ is finite, $\bigcup_{n \in \natp}D_n$ is countable. Given that $G$ is continuous on every point in each $D_n$, $G$ is also continuous on all the discontinuity points of $f$. + + (3): Suppose that $E, F, H$ are locally convex, $G \in BV([a, b]; F)$, and $H$ is complete. Let $f \in \text{Reg}([a, b], G; E)$, then there exists regulated step maps $\net{f} \subset \text{Reg}([a, b], G; E)$ such that $f_\alpha \to f$ uniformly. By \autoref{proposition:rs-complete}, $f \in RS([a, b], G)$. Therefore $\text{Reg}([a, b], G; E) \subset RS([a, b], G)$. + + (4): If $F$ is normed and $G \in BV([a, b]; F)$, then $G$ has at most countably many discontinuities by \autoref{definition:bounded-variation}, so the continuity points of $G$ are dense in $[a, b]$. + + Let $f \in C([a, b]; E)$, then $f \in UC([a, b]; E)$ by \autoref{proposition:uniform-continuous-compact}. Let $U \in \cn_E(0)$, then there exists a partition $P = \bracsn{x_j}_1^n \in \scp([a, b])$ such that for each $1 \le j \le n$ and $x, y \in [x_{j-1}, x_j]$, $f(x) - f(y) \in U$. In which case, let + \[ + \phi = f(a)\one_{\bracs{a}} + \sum_{j = 1}^n f(x_j)\one_{(x_{j - 1}, x_j]} + \] + + then $\phi$ is a regulated step map with $(\phi - f)([a, b]) \in U$. +\end{proof} + +\begin{theorem}[Fundamental Theorem of Calculus for Riemann Integrals] +\label{theorem:ftc-riemann} + Let $[a, b] \subset \real$ and $E$ be a separated locally convex space, then: + \begin{enumerate} + \item For any Riemann integrable function $f: [a, b] \to E$ and $x \in (a, b)$ such that $f$ is continuous at $x$, the function + \[ + F: [a, b] \to E \quad y \mapsto \int_a^y f(t)dt + \] + + is differentiable at $x$ with $DF(x) = f(x)$. + + \item For $F \in C^1([a, b]; E)$, + \[ + F(b) - F(a) = \int_a^b DF(t)dt + \] + \end{enumerate} +\end{theorem} +\begin{proof} + (1): Let $x_0 \in (a, b)$ such that $f$ is continuous at $x$, and $\delta > 0$ such that $(x_0 - \delta, x_0 + \delta) \subset (a, b)$, then for any $h > 0$, + \begin{align*} + \frac{1}{h}\braks{\int_a^{x+h} f(t)dt - \int_a^{x} f(t)dt} &= \frac{1}{h}\int_x^{x+h}f(t)dt \in \overline{\text{Conv}(f([t, t +h)))} \\ + -\frac{1}{h}\braks{\int_a^{x-h} f(t)dt - \int_a^{x} f(t)dt} &= \frac{1}{h}\int_{x-h}^{x}f(t)dt \in \overline{\text{Conv}(f([t, t +h)))} + \end{align*} + + As $E$ is locally convex and separated, and $f$ is continuous at $x$, this implies that $[F(x + h) - F(x)]/h \to f(x)$. + + (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} + diff --git a/src/fa/rs/rs-measure.tex b/src/fa/rs/rs-measure.tex index e8fed0e..248a93a 100644 --- a/src/fa/rs/rs-measure.tex +++ b/src/fa/rs/rs-measure.tex @@ -1,23 +1,92 @@ \section{The Lebesgue-Stieltjes Integral} \label{section:riemann-lebesgue-stieltjes} -\begin{theorem} -\label{theorem:riemann-lebesgue-stieltjes} +\begin{definition}[Lebesgue-Stieltjes Measure] +\label{definition:riemann-lebesgue-stieltjes} Let $[a, b] \subset \real$, $E$ be a Banach space, and $G \in BV([a, b]; E^*)$, then there exists a unique $\mu_G \in M_R([a, b]; E^*)$ such that: \begin{enumerate} - \item For any $f \in C([a, b]; E)$, + \item For any $f \in \text{Reg}([a, b], G; E)$, \[ - \int f(t) G(dt) = \int \dpn{f(t), \mu_G(dt)}{E} + \int_a^b f(t) G(dt) = \int_{[a, b]} \dpn{f(t), \mu_G(dt)}{E} \] - \item For any - - \item For any $a \le c < d \le b$ such that $G$ is continuous on $c$ and $d$, $\mu_G((c, d]) = G(d) - G(c)$. + \item For any $a \le c < d < b$, + \[ + \mu_G((c, d]) = G(d+) - G(c+) = \lim_{z \downto d}G(z) - \lim_{z \downto c}G(z) + \] \end{enumerate} -\end{theorem} -\begin{proof} - (1): By \autoref{proposition:rs-bv-continuous}, the mapping $f \mapsto \int f(t)G(dt)$ is a continuous linear functional on $C_0([a, b]; E) = C([a, b]; E)$. Thus (1) holds by \hyperref[Singer's Representation Theorem]{theorem:singer-representation}. - (2): + The measure $\mu_G$ is the \textbf{Lebesgue-Stieltjes measure} associated with $G$. +\end{definition} +\begin{proof} + By \autoref{proposition:rs-bv-continuous}, the mapping $f \mapsto \int f(t)G(dt)$ is a continuous linear functional on $C_0([a, b]; E) = C([a, b]; E)$. By \hyperref[Singer's Representation Theorem]{theorem:singer-representation}, there exists $\mu_G \in M_R([a, b]; E^*)$ such that (1) holds for $C([a, b], G; E)$. + + (2): Fix $x \in [a, b)$. For each $u \in (x, b)$, there exists a non-increasing function $\phi_u \in C_c([a, b))$ such that $\phi_u|_{[a, x]} = 1$ and $\supp{\phi_u} \subset [a, u]$. By outer regularity of $\mu_G$, + \[ + \mu_G([a, x]) = \lim_{u \downto x}\mu_G([a, u]) = \lim_{u \downto x}\int_{[a, b]}\phi_u d\mu_G = \lim_{u \downto x}\int_a^b \phi_u dG + \] + + For each $u > x$, using \hyperref[integration by parts]{theorem:rs-ibp}, + \begin{align*} + \int_a^b \phi_u dG &= \phi(b)G(b) - \phi(a)G(a) - \int_a^b G d\phi_u \\ + &= - G(a) - \int_a^b G d\phi_u + \end{align*} + + Let $v \in (x, u)$ and $(P = \bracs{x_j}_0^n, c = \bracs{c_j}_1^n)$ be a tagged partition containing $\bracs{x, v, u}$, then since $\phi_u$ is non-increasing, + \begin{align*} + \int_a^b Gd\phi_u &= \sum_{x < x_j \le v}G(c_j)[\phi(x_j) - \phi(x_{j - 1})] + \sum_{v < x_j \le u}G(c_j)[\phi(x_j) - \phi(x_{j - 1})] \\ + &\in [\phi(v) - \phi(x)]G([x, u]) + [\phi(u) - \phi(v)]G((x, u]) \\ + &\subset [\phi(v) - \phi(x)]G([x, u]) - G((x, u]) + \end{align*} + + + Since the above holds for all $v \in (x, u)$, $\int_a^b Gd\phi_u \in -\overline{G((a, u])}$, and + \[ + \int_a^b \phi_u dG \in \overline{G(x, u]} - G(a) + \] + + + As $E^*$ is a Banach space, $G(x+)$ exists by \autoref{proposition:bounded-variation-one-side-limit}, so + \[ + \mu_G([a, x]) = \lim_{u \downto x}\int_a^b \phi_u dG = \bigcap_{u > x}\overline{G((x, u])} - G(a) = G(x+) - G(a) + \] + + + (1): Let $[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)$ with + \[ + \int_a^b x \cdot \one_{[c, d]} dG = x[G(d) - G(c)] = \int_{[a, b]}x \cdot \one_{[c, d]} d\mu_G + \] + + By linearity, for any regulated step map $f: [a, b] \to E$, $\int_a^b f(t) G(dt) = \int_{[a, b]} \dpn{f(t), \mu_G(dt)}{E}$. Therefore (1) holds for $\text{Reg}([a, b], G; E)$ by the \hyperref[Linear Extension Theorem]{theorem:linear-extension-theorem-normed}. +\end{proof} + + +% TODO: Strengthen this to the Lebesgue differentiation case in the future. +% It should work for ALL absolutely continuous functions. + +\begin{proposition} +\label{proposition:lebesgue-stieltjes-differentiable} + Let $[a, b] \subset \real$, $E$ be a normed space, $G \in C^1([a, b]; E^*)$, and $\mu_G \in M_R([a, b]; E^*)$ be the associated Lebesgue-Stieltjes measure, then + \[ + \mu_G(dt) = DG(t)dt + \] +\end{proposition} +\begin{proof} + By the \hyperref[Fundamental Theorem of Calculus]{theorem:ftc-riemann}, for any $[c, d] \subset [a, b]$, + \[ + \int_a^b \one_{[c, d]}dG = \int_a^b \one_{[c, d]} DG(t)dt + \] + + By \autoref{definition:riemann-lebesgue-stieltjes}, applied to both $G$ and $\text{Id}$, + \[ + \int_{[a, b]}\one_{[c, d]}d\mu_G = \int_a^b \one_{[c, d]}dG = \int_a^b \one_{[c, d]} DG(t)dt = \int_{[a, b]} \one_{[c, d]}DG(t)dt + \] + + Thus by linearity, for any regulated step map $f: [a, b] \to E$, + \[ + \int_{[a, b]} f(t) \mu_G(dt) = \int_{[a, b]} \dpn{f(t), DG(t)}{E} dt + \] + + By \autoref{definition:regulated-function}, the regulated step maps are dense in $\text{Reg}([a, b], G; E)$. Therefore by the \hyperref[Linear Extension Theorem]{theorem:linear-extension-theorem-normed}, the above holds for all $f \in \text{Reg}([a, b], G; E)$. By uniqueness of the \hyperref[Lebesgue-Stieltjes measure]{definition:riemann-lebesgue-stieltjes}, $\mu_G(dt) = DG(t)dt$. \end{proof} diff --git a/src/fa/rs/rs.tex b/src/fa/rs/rs.tex index 8225efe..e922a4c 100644 --- a/src/fa/rs/rs.tex +++ b/src/fa/rs/rs.tex @@ -75,28 +75,4 @@ by \autoref{lemma:sum-by-parts}, where $d$ and $Q'$ contain $\seqfz{x_j}$. Thus $(Q', d') \ge P_0$, and $\int_a^b fdG - S(Q', d', G, f) \in U$. \end{proof} -\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 $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 - \[ - \int_a^b x \cdot \one_{[c, d]} dG = x \cdot [G(d) - G(c)] - \] -\end{proposition} -\begin{proof} - Assume without loss of generality that $a < c \le d < b$. Let $U \in \cn_H(0)$, then there exists $V \in \cn_F(0)$ such that $xV \subset U$. By continuity of $G$, there exists $\delta > 0$ such that $G((c - \delta, c]) - G(c) \subset V$ and $G([d, d + \delta)) - G(d) \subset V$. In which case, for any tagged partition $(P = \bracsn{x_j}_0^n, t = \seqf{t_j})$ that contains $\bracs{c - \delta, c, d, d + \delta}$, - \begin{align*} - S(Q, t, x \cdot \one_{[c, d]}, G) &= x\sum_{a < x_j \le c - \delta}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\ - &+ x \sum_{c - \delta < x_j \le c}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\ - &+ x \sum_{c < x_j \le d}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j-1})] \\ - &+ x \sum_{d < x_j \le d + \delta}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\ - &+ x \sum_{d + \delta < x_j \le b}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\ - &= x \sum_{c - \delta \le x_j \le c}\one_{[c, d]}(t_j)[G(x_j) - G(x_{j - 1})] \\ - &+ x \cdot [G(d) - G(c)] \\ - &+ x \sum_{d < x_j \le d + \delta}\one_{[c, d]}[G(x_j) - G(x_{j - 1})] \\ - &\in G(d) - G(c) + xG([c - \delta, c]) + xG([d, d + \delta]) \\ - &\subset x \cdot [G(d) - G(c)] + xV + xV \subset [G(d) - G(c)] + U + U - \end{align*} -\end{proof} diff --git a/src/topology/main/lch.tex b/src/topology/main/lch.tex index 6a85d0c..71da91a 100644 --- a/src/topology/main/lch.tex +++ b/src/topology/main/lch.tex @@ -47,7 +47,7 @@ As $\ol{W}$ is compact, it is normal by \autoref{proposition:compact-hausdorff-normal}. Since $X$ is Hausdorff, $K \subset \ol{W}$ is closed by \autoref{proposition:compact-closed}. - By \hyperref[Urysohn's lemma]{lemma:lch-urysohn}, there exists $f \in C(\ol{V}; [0, 1])$ such that $f|_K = 1$ and $f|_{\ol{W} \setminus V} = 0$. Let + By \hyperref[Urysohn's lemma]{lemma:urysohn}, there exists $f \in C(\ol{V}; [0, 1])$ such that $f|_K = 1$ and $f|_{\ol{W} \setminus V} = 0$. Let \[ F: X \to [0, 1] \quad x \mapsto \begin{cases} f(x) &x \in W \\