Prepare for migration into spec.

This commit is contained in:
Bokuan Li
2026-03-12 21:26:34 -04:00
parent 9139ee3296
commit 61f66523e0
18 changed files with 86 additions and 371 deletions

View File

@@ -1,49 +1,49 @@
\section{Derivatives and Remainders}
\label{section:derivative}
\begin{definition}[Derivatives and Remainders]
\label{definition:derivative-system}
Let $E, F$ be TVSs over $K \in \RC$ and $\ch(E; F), \calr(E; F) \subset F^E$ be vector subspaces, then $\mathcal{HR} = (\ch(E; F), \calr(E; F))$ is a pair of \textbf{derivatives} and \textbf{remainders} if
\begin{enumerate}
\item[(T)] For any $T \in \ch$, if there exists $V \in \cn_E(0)$ and $r \in \calr$ such that $T|_V = r|_V$, then $T = 0$.
\end{enumerate}
\end{definition}
\begin{definition}[$\mathcal{HR}$-Differentiability]
\label{definition:space-differentiability}
Let $E, F$ be TVSs over $K \in \RC$, $\mathcal{HR}$ be a pair of derivatives and remainders, $U \subset E$ be open, $f: U \to F$ be a function, and $x_0 \in U$, then $f$ is \textbf{$\mathcal{HR}$-differentiable} at $x_0$ if there exists $V \in \cn_E(0)$, $T \in \ch$, and $r \in \calr$ such that
\[
f(x_0 + h) = f(x_0) + Th + r(h)
\]
for all $h \in V$. In which case, $T = D_{\mathcal{HR}}f(x_0)$ is the unique element of $\ch$ satisfying the above, known as the \textbf{$\mathcal{HR}$-derivative} of $f$ at $x_0$.
\end{definition}
\begin{proof}
Let $S, T \in \ch$, $r, s \in \calr$, and $V \in \cn_E(0)$ such that
\[
f(x_0 + h) - f(x_0) = Sh + r(h) = Th + s(h)
\]
for all $h \in V$, then $(S - T)(h) = (s - r)(h)$. By (T), $S - T = 0$. Hence $S = T$.
\end{proof}
\begin{proposition}
\label{proposition:derivative-linearity}
Let $E, F$ be TVSs over $K \in \RC$, $\mathcal{HR}$ be a pair of derivatives and remainders, $U \subset E$ be open, $f, g: U \to F$ be functions, and $x_0 \in U$. If $f, g$ are $\mathcal{HR}$-differentiable at $x_0$, then for any $\lambda \in K$, $\lambda f + g$ is $\mathcal{HR}$-differentiable at $x_0$, and
\[
D_{\mathcal{HR}}(\lambda f + g)(x_0) = \lambda D_{\mathcal{HR}}f(x_0) + D_{\mathcal{HR}}g(x_0)
\]
\end{proposition}
\begin{proof}
Let $V \in \cn_E(0)$ and $r, s \in \calr$ such that
\begin{align*}
f(x_0 + h) - f(x_0) &= D_{\mathcal{HR}}f(x_0)h + r(h) \\
g(x_0 + h) - f(x_0) &= D_{\mathcal{HR}}g(x_0)h + s(h)
\end{align*}
then
\[
(\lambda f + g)(x_0+h) - (\lambda f + g)(x_0) = \underbrace{[\lambda D_{\mathcal{HR}}f(x_0) + D_{\mathcal{HR}}g(x_0)]}_{\in \ch}h + \underbrace{(\lambda r + s)}_{\in \calr}(h)
\]
\end{proof}
\section{Derivatives and Remainders}
\label{section:derivative}
\begin{definition}[Derivatives and Remainders]
\label{definition:derivative-system}
Let $E, F$ be TVSs over $K \in \RC$ and $\ch(E; F), \calr(E; F) \subset F^E$ be vector subspaces, then $\mathcal{HR} = (\ch(E; F), \calr(E; F))$ is a pair of \textbf{derivatives} and \textbf{remainders} if
\begin{enumerate}
\item[(T)] For any $T \in \ch$, if there exists $V \in \cn_E(0)$ and $r \in \calr$ such that $T|_V = r|_V$, then $T = 0$.
\end{enumerate}
\end{definition}
\begin{definition}[$\mathcal{HR}$-Differentiability]
\label{definition:space-differentiability}
Let $E, F$ be TVSs over $K \in \RC$, $\mathcal{HR}$ be a pair of derivatives and remainders, $U \subset E$ be open, $f: U \to F$ be a function, and $x_0 \in U$, then $f$ is \textbf{$\mathcal{HR}$-differentiable} at $x_0$ if there exists $V \in \cn_E(0)$, $T \in \ch$, and $r \in \calr$ such that
\[
f(x_0 + h) = f(x_0) + Th + r(h)
\]
for all $h \in V$. In which case, $T = D_{\mathcal{HR}}f(x_0)$ is the unique element of $\ch$ satisfying the above, known as the \textbf{$\mathcal{HR}$-derivative} of $f$ at $x_0$.
\end{definition}
\begin{proof}
Let $S, T \in \ch$, $r, s \in \calr$, and $V \in \cn_E(0)$ such that
\[
f(x_0 + h) - f(x_0) = Sh + r(h) = Th + s(h)
\]
for all $h \in V$, then $(S - T)(h) = (s - r)(h)$. By (T), $S - T = 0$. Hence $S = T$.
\end{proof}
\begin{proposition}
\label{proposition:derivative-linearity}
Let $E, F$ be TVSs over $K \in \RC$, $\mathcal{HR}$ be a pair of derivatives and remainders, $U \subset E$ be open, $f, g: U \to F$ be functions, and $x_0 \in U$. If $f, g$ are $\mathcal{HR}$-differentiable at $x_0$, then for any $\lambda \in K$, $\lambda f + g$ is $\mathcal{HR}$-differentiable at $x_0$, and
\[
D_{\mathcal{HR}}(\lambda f + g)(x_0) = \lambda D_{\mathcal{HR}}f(x_0) + D_{\mathcal{HR}}g(x_0)
\]
\end{proposition}
\begin{proof}
Let $V \in \cn_E(0)$ and $r, s \in \calr$ such that
\begin{align*}
f(x_0 + h) - f(x_0) &= D_{\mathcal{HR}}f(x_0)h + r(h) \\
g(x_0 + h) - f(x_0) &= D_{\mathcal{HR}}g(x_0)h + s(h)
\end{align*}
then
\[
(\lambda f + g)(x_0+h) - (\lambda f + g)(x_0) = \underbrace{[\lambda D_{\mathcal{HR}}f(x_0) + D_{\mathcal{HR}}g(x_0)]}_{\in \ch}h + \underbrace{(\lambda r + s)}_{\in \calr}(h)
\]
\end{proof}