Adjusted mean value theorem.

src/dg/derivative/mvt.tex

@@ -75,7 +75,7 @@
 
 
 \begin{theorem}[Mean Value Theorem]
-\label{theorem:mean-value-theorem}
+\label{theorem:mean-value-theorem-line}
     Let $-\infty < a < b < \infty$, $E$ be a separated locally convex space, $S \subset [a, b]$ be at most countable, and $f \in C([a, b]; E)$ be differentiable on $(a, b) \setminus N$, then
     \[
     f(b) - f(a) \in \overline{\text{Conv}\bracs{Df(x)(b - a)| x \in (a, b) \setminus N}}
@@ -84,7 +84,7 @@
 \begin{proof}
     By \ref{proposition:derivative-sets-real}, $f$ is right-differentiable on $(a, b) \setminus N$ with
     \[
-    D^+f(x) = Df(x) \in \bracs{Df(x)|x \in (a, b) \setminus N}
+    D^+f(x) = Df(x) \in \bracs{Df(y)|y \in (a, b) \setminus N}
     \]
     for all $x \in (a, b)$. Let $g(x) = x$, then by \ref{theorem:right-differentiable-convex-form},
     \[
@@ -92,16 +92,37 @@
     \]
 \end{proof}
 
+\begin{theorem}[Mean Value Theorem]
+\label{theorem:mean-value-theorem}
+    Let $E$ be a topological vector space, $F$ be a separated locally convex space, $V \subset E$ be open and star shaped at $x \in V$, $f: V \to F$ be Gateau-differentiable on $V$, then for any $y \in V$,
+    \[
+    f(y) - f(x) \in \overline{\text{Conv}\bracs{Df(z)(y - x)|z \in (x, y)}}
+    \]
+    where $[x, y] = \bracs{(1 - t)x + ty|y \in [0, 1]}$.
+\end{theorem}
+\begin{proof}
+    Let $g: [0, 1] \to F$ be defined by $g(t) = f((1 - t)x + ty)$. Since $f$ is Gateaux-differentiable, $g$ is differentiable by the chain rule \ref{proposition:chain-rule-sets-conditions} with $Dg(t) = Df((1 - t)x + ty)(y - x)$, and continuous by \ref{proposition:derivative-sets-real}.
+
+    By the Mean Value Theorem (\ref{theorem:mean-value-theorem-line}),
+    \[
+    f(y) - f(x) = g(1) - g(0) \in \overline{\text{Conv}\bracs{Dg(t)|t \in [0, 1]}} = \overline{\text{Conv}\bracs{Df(z)(y - x)|z \in (x, y)}}
+    \]
+\end{proof}
+
 \begin{proposition}
 \label{proposition:zero-derivative-constant}
     Let $E$ be a topological vector space, $F$ be a separated locally convex space, $V \subset E$ be open and connected, $f: V \to F$ be Gateaux-differentiable on $V$ such that $Df(x) = 0$ for all $x \in V$, then $f$ is constant.
 \end{proposition}
 \begin{proof}
-    Let $x, y \in V$ such that $\bracs{(1 - t)x + ty|t \in [0, 1]} \subset V$. Since $f$ is Gateaux-differentiable, $g: [0, 1] \to F$ defined by $g(t) = f((1 - t)x + ty)$ is differentiable with $Dg(t) = 0$ for all $t \in [0, 1]$. By the Mean Value Theorem (\ref{theorem:mean-value-theorem}), $f(y) - f(x) = 0$.
+    Let $x \in V$, then for any $U \in \cn(0)$ circled with $U + x \subset V$ and $y \in U + x$,
+    \[
+    f(y) - f(x) \in \overline{\text{Conv}\bracs{Df(z)(y - x)|z \in (x, y)}} = \bracs{0}
+    \]
+    by the Mean Value Theorem (\ref{theorem:mean-value-theorem-line}).
 
-    Fix $x \in V$ and let $W$ be the connected component of $\bracs{y \in V|f(x) = f(y)}$ containing $x$. Since $E$ is locally path-connected (\ref{proposition:tvs-locally-connected}), $W$ is open.
+    Fix $x \in V$ and let $W$ be the connected component of $\bracs{y \in V|f(x) = f(y)}$ containing $x$. For any $y \in W$, by \ref{proposition:tvs-good-neighbourhood-base}, there exists $U \in \cn(0)$ circled such that $U + y \subset V$. Therefore $W \supset W \cup (U + y)$, and $W$ is open by \ref{lemma:openneighbourhood}.
 
-    Let $y \in \overline{W}$. By \ref{proposition:tvs-good-neighbourhood-base}, there exists $U \in \cn_E(0)$ radial such that $U + y \subset V$. Since any point in $U$ is joined to $y$ via a line segment, $f$ is constant on $U + y$. As $y \in \overline{W}$, $U + y \cap W \ne \emptyset$, so $y \in W$.
+    For any $y \in \ol W \cap V$, there exists $U \in \cn(0)$ circled such that $U + y \subset V$. As $y \in \ol W \cap V$, $U \cap W \ne \emptyset$. Thus $f(y) = f(x)$, $y \in W$, and $W$ is relatively closed.
 
-    Since $W$ is both open and closed, $W$ must coincide with $V$.
+    Since $V$ is connected and $W \subset V$ is both open and closed, $W = V$.
 \end{proof}