avewright/proofwiki-math huggingface dataset:
Theorem: Supremum Operator Norm is Well-Defined

Let $K$ be a field.
Let $X, Y$ be normed vector spaces over $K$.
Let $\map {CL} {X, Y}$ be the continuous linear transformation space.
Let $\norm {\, \cdot \,}$ be an operator norm on $\map {CL} {X, Y}$ defined as:
:$\norm T := \map \sup {\norm {Tx} : x \in X : \norm x \le 1}$
Then $\norm {\, \cdot \,}$ is well-defined.

Proof:
Let $S = \set {\norm {T x} : x \in X : \norm x \le 1}$
By definition of the norm:
:$S \subseteq \R$
Theorem: Equivalence of Defintions of Ergodic Measure-Preserving Transformation

Let $\struct {X, \BB, \mu}$ be a probability space.
Let $T: X \to X$ be a measure-preserving transformation.
{{TFAE|def = Ergodic Measure-Preserving Transformation}}

Proof:
=== Definition 1 implies Definition 2 ===
First, we claim that for each $j \in \N$:
:$\map \mu {T^{-j} \sqbrk A \symdif A} = 0$.
Indeed, applying Symmetric Difference is Subset of Union of Symmetric Differences, inductively:
{{begin-eqn}}
{{eqn | l = T^{-j} \sqbrk A \symdif A
      | o = \subseteq
      | r = \bigcup _{i = 0} ^{j-1} T^{-\paren {i+1} }\sqbrk A \symdif T^{-i} \sqbrk A
}}
{{eqn | r = \bigcup _{i = 0} ^{j-1} T^{-i} \sqbrk {T^{-1} \sqbrk A \symdif A}
}}
{{end-eqn}}
so that:
{{begin-eqn}}
{{eqn | l = \map \mu {T^{-j} \sqbrk A \symdif A}
      | o = \le
      | r = \sum _{i = 0} ^{j-1} \map \mu { T^{-i} \sqbrk {T^{-1} \sqbrk A \symdif A} }
}}
{{eqn | r = \sum _{i = 0} ^{j-1} \map \mu { T^{-1} \sqbrk A \symdif A }
}}
{{eqn | r = 0}}
{{end-eqn}}
Next, let:
:$\ds A_\infty := \bigcap _{N \mathop \ge 1} \bigcup _{j \mathop \ge N} T^{-j} \sqbrk A$
Then $A_\infty \in \set {0, 1}$, since:
:$T^{-1} \sqbrk {A_\infty} = A_\infty$
Therefore, we shall show $\map \mu A = \map \mu {A_\infty}$.
Observe:
{{begin-eqn}}
{{eqn | l = \map \mu {A_\infty}
      | r = \map \mu {\bigcap _{N \mathop \ge 1} \bigcup _{j \mathop \ge N} T^{-j} \sqbrk A}
}}
{{eqn | r = \lim _{N \to \infty} \map \mu {\bigcup _{j \mathop \ge N} T^{-j} \sqbrk A}
}}
{{eqn | r = \lim _{N \to \infty} \map \mu {T^{-N} \sqbrk {\bigcup _{j \mathop \ge 0} T^{-j} \sqbrk A} }
}}
{{eqn | r = \lim _{N \to \infty} \map \mu {\bigcup _{j \mathop \ge 0} T^{-j} \sqbrk A}
}}
{{eqn | r = \map \mu {\bigcup _{j \mathop \ge 0} T^{-j} \sqbrk A}
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = 0
      | o = \le
      | r = \map \mu {A_\infty} - \map \mu A
}}
{{eqn | r = \map \mu { \paren {\bigcup _{j \mathop \ge 0} T^{-j} \sqbrk A} \setminus A}
}}
{{eqn | r = \map \mu {\bigcup _{j \mathop \ge 0} \paren { T^{-j} \sqbrk A \setminus A} }
}}
{{eqn | o = \le
      | r = \sum _{j \mathop \ge 0} \map \mu {T^{-j} \sqbrk A \setminus A}
}}
{{eqn | r = 0 }}
{{end-eqn}}
{{qed|lemma}}
Theorem: Quasilinear Differential Equation/Examples/x + y y' = 0

The first order quasilinear ordinary differential equation over the real numbers $\R$:
:$x + y y' = 0$
has the general solution:
:$x^2 + y^2 = C$
where:
:$C > 0$
:$y \ne 0$
:$x < \size {\sqrt C}$
with the singular point:
:$x = y = 0$

Proof:
Let us rearrange the equation in question:
{{begin-eqn}}
{{eqn | l = x + y y'
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y \dfrac {\d y} {\d x}
      | r = -x
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y \rd y
      | r = \paren {-1} x \rd x
      | c = 
}}
{{end-eqn}}
This is in the form:
:$y \rd y = k x \rd x$
where $k = 1$.
From First Order ODE: $y \rd y = k x \rd x$:
:$y^2 = \paren {-1} x^2 + C$
from which the result follows.
{{qed}}
Theorem: Quasilinear Differential Equation/Examples/x + y y' = 0

The first order quasilinear ordinary differential equation over the real numbers $\R$:
:$x + y y' = 0$
has the general solution:
:$x^2 + y^2 = C$
where:
:$C > 0$
:$y \ne 0$
:$x < \size {\sqrt C}$
with the singular point:
:$x = y = 0$

Proof:
Observe that from Derivative of Power and Chain Rule for Derivatives:
:$\dfrac {\map \d {x^2 + y^2} } {\d y} = 2 x + 2 y \dfrac {\d y} {\d x}$
Hence:
:$\dfrac {\map \d {x^2 + y^2} } {\d y} = 0$
So from Derivative of Constant:
:$x^2 + y^2 = C$
where $C$ is abitrary.
{{qed}}
Theorem: Quasilinear Differential Equation/Examples/x + y y' = 0/Explicit Solution

The first order quasilinear ordinary differential equation:
:$x + y y' = 0$
has a general solution which can be expressed explicitly as:
:$y = \pm \sqrt {C - x^2}$
over the domain:
:$-\sqrt C < x < \sqrt C$

Proof:
The general solution of $x + y y' = 0$ is implicitly over the real numbers.
We have:
{{begin-eqn}}
{{eqn | l = x^2 + y^2
      | r = y
      | c = Quasilinear Differential Equation: $x + y y' = 0$
}}
{{eqn | ll= \leadsto
      | l = y^2
      | r = C - x^2
      | c = where $C - x^2 \ge 0$
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \pm \sqrt {C - x^2}
      | c = where $\size {\sqrt C} \ge x$
}}
{{end-eqn}}
But when $y = 0$, the derivative $y'$ of the ordinary differential equation $x + y y' = 0$ needs to be infinite for non-zero $x$.
Hence:
:$-\sqrt C < x < \sqrt C$
{{Qed}}
Theorem: Universal Upper Bound greater than Supremum Operator Norm

Let $\map {CL} {X, Y}$ be the continuous linear transformation space.
Let $T \in \map {CL} {X, Y}$.
Let $\norm {\, \cdot \,}$ be an operator norm on $\map {CL} {X, Y}$ defined as:
:$\norm T := \sup \set {\norm {Tx}_Y : x \in X : \norm x_X \le 1}$
Suppose:
:$\exists M \in \R_{> 0} : \forall x \in X : \norm {T x}_Y \le M \norm x_X$
Then:
:$\norm {T} \le M$

Proof:
Let $x \in X$ be such that $\norm x_X \le 1$.
Then:
{{begin-eqn}}
{{eqn | l = \norm {T x}_Y
      | o = \le 
      | r = M \norm x_X
}}
{{eqn | o = \le
      | r = M \cdot 1
}}
{{eqn | r = M
}}
{{end-eqn}}
Hence, $M$ is an upper bound for $S = \set {\norm {T x}_Y : x \in X : \norm x_X \le 1}$.
By definition of the supremum of subset of real numbers:
:$\sup S \le M$.
That is:
:$\norm T \le M$.
{{qed}}
Theorem: Supremum Operator Norm as Universal Upper Bound

Let $\map {CL} {X, Y}$ be the continuous linear transformation space.
Let $T \in \map {CL} {X, Y}$.
Let $\norm {\, \cdot \,}$ be the supremum operator norm on $\map {CL} {X, Y}$.
Then:
:$\forall x \in X : \norm {Tx}_Y \le \norm T \norm x_X$

Proof:
Let $S = \set {\norm {Tx}_Y : x \in X : \norm x_X \le 1}$.
Suppose $x = \mathbf 0$.
Then:
{{begin-eqn}}
{{eqn | l = \norm {T x}_Y
      | r = \norm {T \mathbf 0}_Y
}}
{{eqn | r = \norm {\mathbf 0}_Y
}}
{{eqn | r = 0
}}
{{eqn | r = \norm T 0
}}
{{eqn | r = \norm T \norm {\mathbf 0}_X
}}
{{eqn | r = \norm T \norm x_X
}}
{{end-eqn}}
Suppose $x \ne \mathbf 0$.
Let $\hat x \in X$ such that:
:$\ds \hat x = \frac x {\norm x_X}$
Then:
:$\ds \norm {\hat x}_X = \frac {\norm x_X}{\norm x_X} = 1$.
Thus:
:$\norm {T \hat x}_Y \in S$
and 
$\norm {T \hat x}_Y \le \sup S = \norm T$
Furthermore:
{{begin-eqn}}
{{eqn | l = \frac {\norm {Tx}_Y }{\norm x_X}
      | r = \norm {\frac {Tx}{\norm x_X} }_Y
      | c = {{Defof|Norm on Vector Space}}
}}
{{eqn | r = \norm {\map T {\frac x {\norm x_X} } }_Y
      | c = {{Defof|Linear Transformation on Vector Space}}
}}
{{eqn | r = \norm {T \hat x}_Y
}}
{{eqn | o = \le
      | r = \norm T
}}
{{end-eqn}}
Rearranging, we get:
:$\norm {T x}_Y \le \norm T \norm x_X$
{{qed}}
Theorem: Reversed Complex Contour is Contour

Let $C$ be a contour in the complex plane $\C$ that is defined as a concatenation of a finite sequence $\sequence{ C_1, \ldots, C_n }$ of directed smooth curves in $\C$.
Then the finite sequence of reversed directed smooth curves:
:$\sequence{ -C_n, -C_{n - 1}, \ldots, -C_1 }$
defines a contour that is independent of the parameterization of $C_1, \ldots, C_n$.

Proof:
Let $C_k$ be parameterized by the smooth path $\gamma_k: \closedint {a_k} {b_k} \to \C$ for all $k \in \set {1, \ldots, n}$.
From Reversed Directed Smooth Curve is Directed Smooth Curve, it follows that $-C_k$ is independent of the parameterization $\gamma_k$ of $C_k$.
We now prove that the end point of $-C_k$ is equal to the start point of $-C_{k - 1}$ for all $k \in \set {2, \ldots, n}$.
By definition of reversed directed smooth curve, $-C_k$ is parameterized by $\rho_k: \closedint {a_k} {b_k} \to \C$, defined by $\map {\rho_k} t = \map {\gamma_k} {a_k + b_k - t}$.
From Reparameterization of Directed Smooth Curve Maps Endpoints To Endpoints, it follows that the endpoints $\map {\rho_k} {a_k}$ and $\map {\rho_k} {b_k}$ are independent of the parameterization $\rho_k$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\rho_k} {b_k}
      | r = \map {\gamma_k} {a_k + b_k - b_k}
}}
{{eqn | r = \map {\gamma_k} {a_k}
}}
{{eqn | r = \map {\gamma_{k - 1} } {b_{k - 1} }
      | c = {{Defof|Contour (Complex Plane)}}
}}
{{eqn | r = \map {\rho_{k - 1} } {a_{k - 1} }
}}
{{end-eqn}}
By definition, it follows that $-C_n, \ldots, -C_1$ can be concatenated to form a contour.
{{qed}}
Theorem: Composite of Strictly Increasing Mappings is Strictly Increasing

Let $\struct {S_1, \preceq_1}$, $\struct {S_2, \preceq_2}$ and $\struct {S_3, \preceq_3}$ be ordered sets.
Let:
:$\phi: \struct {S_1, \preceq_1} \to \struct {S_2, \preceq_2}$
and:
:$\psi: \struct {S_2, \preceq_2} \to \struct {S_3, \preceq_3}$
be strictly increasing mappings.
Then $\psi \circ \phi: \struct {S_1, \preceq_1} \to \struct {S_3, \preceq_3}$ is also a strictly increasing mapping.

Proof:
By definition of composition of mappings:
:$\map {\paren {\psi \circ \phi} } x = \map \psi {\map \phi x}$
As $\phi$ is a strictly increasing mapping, we have:
:$\forall x_1, y_1 \in S_1: x_1 \prec_1 y_1 \implies \map \phi {x_1} \prec_2 \map \phi {y_1}$
where $a \prec_1 b$ denotes that $a \preceq_1 b$ and $a \ne b$.
As $\psi$ is a strictly increasing mapping, we have:
:$\forall x_2, y_2 \in S_2: x_2 \prec_2 y_2 \implies \map \psi {x_2} \prec_3 \map \psi {y_2}$
where $a \prec_2 b$ denotes that $a \preceq_2 b$ and $a \ne b$.
By setting $x_2 = \map \phi {x_1}, y_2 = \map \phi {y_1}$, it follows that:
:$\forall x_1, y_1 \in S_1: x_1 \prec_1 y_1 \implies \map \psi {\map \phi {x_1} } \prec_3 \map \psi {\map \phi {y_1} }$
That is:
:$\forall x_1, y_1 \in S_1: x_1 \prec_1 y_1 \implies \map {\paren {\psi \circ \phi} } {x_1} \prec_3 \map {\paren {\psi \circ \phi} } {y_1}$
Hence the result.
{{qed}}
Category:Increasing Mappings
h8dq9wme9ks7cledqea5zzdx1b4uwi1
Theorem: Primitive of Reciprocal of 1 plus x squared/Arctangent Form

:$\ds \int \frac {\d x} {1 + x^2} = \arctan x + C$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\arctan x}
      | r = \dfrac 1 {1 + x^2}
      | c = Derivative of Arctangent Function
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d x} {1 + x^2} 
      | r = \arctan x + C
      | c = {{Defof|Primitive (Calculus)}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Root of 1 minus x squared/Arcsine Form

:$\ds \int \frac {\d x} {\sqrt {1 - x^2} } = \arcsin x + C$

Proof:
From Primitive of $\dfrac 1 {\sqrt {a^2 - x^2} }$: Arcsine Form:
:$\ds \int \frac {\d x} {\sqrt {a^2 - x^2} } = \arcsin \frac x a + C$
The result follows by setting $a = 1$.
{{Qed}}
Theorem: Primitive of Reciprocal of Root of 1 minus x squared/Arcsine Form

:$\ds \int \frac {\d x} {\sqrt {1 - x^2} } = \arcsin x + C$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\arcsin x}
      | r = \dfrac 1 {\sqrt {1 - x^2} }
      | c = Derivative of Arcsine Function
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d x} {\sqrt {1 - x^2} } 
      | r = \arcsin x + C
      | c = {{Defof|Primitive (Calculus)}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sine Function is Absolutely Convergent/Complex Case

The complex sine function $\sin: \C \to \C$ is absolutely convergent.

Proof:
The definition of the complex sine function is:
:$\ds \forall z \in \C: \sin z = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {z^{2 n + 1} } {\paren {2 n + 1}!}$
By definition of absolutely convergent complex series, we must show that the power series
:$\ds \sum_{n \mathop = 0}^\infty \size {\paren {-1}^n \frac {z^{2 n + 1} } {\paren {2 n + 1}!} }$
is convergent.
We have
{{begin-eqn}}
{{eqn | l = \ds \sum_{n \mathop = 0}^\infty \size {\paren {-1}^n \frac {z^{2 n + 1} } {\paren {2 n + 1}!} }
      | r = \sum_{n \mathop = 0}^\infty \frac {\size z^{2 n + 1} } {\paren {2 n + 1}!}
      | c = {{Defof|Complex Modulus}} {{explain|If we need this step explained, then it needs to be broken out into a series of steps that illustrates that the complex modulus is absolutely multiplicative, or whatever, and of course that $\size {\paren {-1}^n} {{=}} 1$. That is, if we are going to bother doing that here.}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren{ \frac {\size z^{2 n + 1} } {\paren {2 n + 1}!} + \frac {\size z^{2 n } } {\paren {2 n }!} }
      | c = Squeeze Theorem for Complex Sequences
      | o = \le
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\size z^n} {n!}
      | c = changing indices }}
{{eqn | r = \exp \size z
      | c = Taylor Series Expansion for Exponential Function }}
{{end-eqn}}
The result follows from Squeeze Theorem for Complex Sequences.
{{qed}}
Theorem: Sine Function is Absolutely Convergent/Complex Case

The complex sine function $\sin: \C \to \C$ is absolutely convergent.

Proof:
Radius of Convergence of Power Series Expansion for Sine Function shows that the radius of convergence of the complex sine function is infinite.
Then Existence of Radius of Convergence of Complex Power Series shows that the complex sine function is absolutely convergent.
{{qed}}
Theorem: Cosine Function is Absolutely Convergent/Complex Case

The complex cosine function $\cos: \C \to \C$ is absolutely convergent.

Proof:
The definition of the complex cosine function is:
:$\ds \cos z = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {z^{2 n} } {\paren {2 n}!}$
By definition of absolutely convergent complex series, we must show that the power series
:$\ds \sum_{n \mathop = 0}^\infty \size {\paren {-1}^n \frac {z^{2 n} } {\paren {2 n}!} }$
is convergent.
We have
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 0}^\infty \size {\paren {-1}^n \frac {z^{2 n} } {\paren {2 n}!} }
      | r = \sum_{n \mathop = 0}^\infty \frac {\size z^{2 n} } {\paren {2 n}!}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren{ \frac {\size z^{2 n} } {\paren {2 n}!} + \frac {\size z^{2 n + 1} } {\paren {2 n + 1}!} }
      | c = Squeeze Theorem for Complex Sequences
      | o = \leq
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\size z^n} {n!}
      | c = changing indices }}
{{eqn | r = \exp \size z
      | c = Taylor Series Expansion for Exponential Function }}
{{end-eqn}}
The result follows from Squeeze Theorem for Complex Sequences.
{{qed}}
Theorem: Cosine Function is Absolutely Convergent/Complex Case

The complex cosine function $\cos: \C \to \C$ is absolutely convergent.

Proof:
Radius of Convergence of Power Series Expansion for Cosine Function shows that the radius of convergence of the complex cosine function is infinite.
Then Existence of Radius of Convergence of Complex Power Series shows that the complex cosine function is absolutely convergent.
{{qed}}
Theorem: Contour Integral of Closed Contour Split into Two Contours

Let $f: D \to \C$ be a continuous complex function, where $D$ is a connected domain.
Let $C = \sequence {C_1, \ldots, C_n}$ be a closed contour in $D$.
Let $C'$ be a contour in $D$ with start point $z_1$ and end point $z_2$.
Let $-C'$ denote the reversed contour of $C'$.
Suppose:
:$z_1$ is equal to the end point of $C_{k_1}$
and:
:$z_2$ is equal to the end point of $C_{k_2}$ for some $k_1, k_2 \in \set {1, 2, \ldots, n}$ with $k_1 < k_2$.
Define two contours $C^{\paren 1}, C^{\paren 2}$ by concatenation as 
:$C^{\paren 1} = \sequence {C_1, \ldots, C_{k_1}, C', C_{k_2 + 1}, \ldots, C_n}$
:$C^{\paren 2} = \sequence {C_{k_1 + 1}, \ldots, C_{k_2}, -C'}$
Then:
:$\ds \oint_C \map f z \rd z = \oint_{C^{\paren 1} } \map f z \rd z + \oint_{C^{\paren 2} } \map f z \rd z$

Proof:
By definition of closed contour, $C^{\paren 1}$ and $C^{\paren 2}$ are closed contours.
Then:
{{begin-eqn}}
{{eqn | l = \oint_C \map f z \rd z
      | r = \sum_{j \mathop = 1}^n \int_{C_j} \map f z \rd z
      | c = Contour Integral of Concatenation of Contours
}}
{{eqn | r = \sum_{j \mathop = 1}^n \int_{C_j} \map f z \rd z + \int_{C'} \map f z \rd z + \int_{-C'} \map f z \rd z
      | c = Contour Integral along Reversed Contour
}}
{{eqn | r = \paren {\sum_{j \mathop = 1}^{k_1} \int_{C_j} \map f z \rd z + \int_{C'} \map f z \rd z + \sum_{j \mathop = k_2 + 1}^n \int_{C_j} \map f z \rd z} + \paren {\sum_{j \mathop = k_1 + 1}^{k_2} \int_{C_j} \map f z \rd z + \int_{-C'} \map f z \rd z}
}}
{{eqn | r = \oint_{C^{\paren 1} }\map f z \rd z + \oint_{C^{\paren 2} } \map f z \rd z
      | c = Contour Integral of Concatenation of Contours
}}
{{end-eqn}}
{{qed}}
Theorem: Power Series Expansion for Exponential Integral Function/Formulation 2

Let $\Ei: \R_{>0} \to \R$ denote the exponential integral function:
:$\map \Ei x = \ds \int_{t \mathop \to -\infty}^{t \mathop = x} \frac {e^t} t \rd t$
Then:
{{begin-eqn}}
{{eqn | l = \map \Ei x
      | r = \gamma + \ln x + \sum_{n \mathop = 1}^\infty \frac {x^n} {n \times n!}
      | c = 
}}
{{eqn | r = \gamma + \ln x + \frac x {1 \times 1!} + \frac {x^2} {2 \times 2!} + \frac {x^3} {3 \times 3!} + \cdots
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map \Ei x
      | r = \gamma + \ln x + \int_0^x \frac {e^u - 1} u \rd u
      | c = Characterization of Exponential Integral Function
}}
{{eqn | r = \gamma + \ln x + \int_0^x \frac 1 u \paren {\sum_{n \mathop = 0}^\infty \frac {u^n} {n!} - 1} \rd u
      | c = {{Defof|Real Exponential Function}}
}}
{{eqn | r = \gamma + \ln x + \int_0^x \frac 1 u \paren {\sum_{n \mathop = 1}^\infty \frac {u^n} {n!} } \rd u
}}
{{eqn | r = \gamma + \ln x + \sum_{n \mathop = 1}^\infty \frac 1 {n!} \paren {\int_0^x u^{n - 1} \rd u}
      | c = Power Series is Termwise Integrable within Radius of Convergence
}}
{{eqn | r = \gamma + \ln x + \sum_{n \mathop = 1}^\infty \frac {x^n} {n \times n!}
      | c = Primitive of Power
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Logarithm Function is Transcendental

Let $a \in \R_{>0}$ be a strictly positive real number such that $a \ne 1$.
Let $\log_a: \C \to \C$ denote the complex general logarithm base $a$.
$\log_a$ is a transcendental function.

Proof:
{{ProofWanted}}
Category:Logarithms
Category:Examples of Transcendental Functions
r8kquxl6v4xuy1lgbml72nv66z0epn1
Theorem: Epsilon-Function Differentiability Condition/Complex Case

Let $f: D \to \C$ be a continuous function, where $D \subseteq \C$ is an open set.
Let $z \in \C$.
Then $f$ is differentiable at $z$ {{iff}} there exist $\alpha \in \C$ and $r \in \R_{>0}$ such that for all $h \in \map {B_r} 0 \setminus \set 0$:
:$\map f {z + h} = \map f z + h \paren {\alpha + \map \epsilon h}$
where:
:$\map {B_r} 0$ denotes an open ball of $0$
:$\epsilon: \map {B_r} 0 \setminus \set 0 \to \C$ is a complex function with $\ds \lim_{h \mathop \to 0} \map \epsilon h = 0$.
If the conditions are true, then $\alpha = \map {f'} z$.

Proof:
=== Necessary Condition ===
Assume that $f$ is differentiable in $z$.
By definition of open set, there exists $r \in \R_{>0}$ such that the open ball $\map {B_r} z \subseteq D$.
Define $\epsilon: \map {B_r} 0 \setminus \set 0 \to \C$ by:
:$\map \epsilon h = \dfrac {\map f {z + h} - \map f z} h - \map {f'} z$
Let $h \in \map {B_r} 0 \setminus \set 0$.
Then:
:$z + h \in \map {B_r} z \setminus \set z \subseteq D$
so $\epsilon$ is well-defined.
As $f$ is differentiable in $z$, it follows that:
:$\ds \lim_{h \mathop \to 0} \map \epsilon h = \lim_{h \mathop \to 0} \dfrac {\map f {z + h} - \map f z} h - \map {f'} z = \map {f'} z - \map {f'} z = 0$
Let us put $\alpha = \map {f'} z$.
It follows that for all $h \in \map {B_r} 0 \setminus \set 0$:
:$\map f {z + h} = \map f z + h \paren {\alpha + \map \epsilon h}$
{{qed|lemma}}
Theorem: Supremum Operator Norm is Norm

Let $\map {CL} {X, Y}$ be the continuous linear transformation space.
Let $\norm {\, \cdot \,} : \map {CL} {X, Y} \to \R$ be the supremum operator norm such that:
:$\forall T \in \map {CL} {X, Y} : \norm T := \sup \set {\norm {Tx}_Y : x \in X : \norm x_X \le 1}$
Then $\norm {\, \cdot \,}$ is a norm.

Proof:
=== Positive definiteness ===
Let $T \in \map {CL} {X, Y}$.
By definition of norm:
:$\norm {Tx}_Y \ge 0$
Then:
:$\ds \norm T = \sup_{\begin{split} x \mathop \in X \\ \norm x \mathop \le 1 \end{split} } \norm {T x}_Y \ge 0$
Suppose $\norm T = 0$.
Then:
{{begin-eqn}}
{{eqn | l = \norm {T x}_Y 
      | o = \le 
      | r = \norm T \norm x_X 
      | c = Supremum Operator Norm as Universal Upper Bound
}}
{{eqn | r = 0 \cdot \norm x_X 
}}
{{eqn | r = 0
}}
{{end-eqn}}
Hence:
:$\norm {T x}_Y = 0$
By Norm Axiom $N1$: 
:$\forall x \in X : Tx = \mathbf 0_Y$
where $\mathbf 0_Y$ is the zero vector in the normed vector space $Y$.
Therefore:
:$T = \mathbf 0$.
{{qed|lemma}}
Theorem: Combination Theorem for Complex Derivatives/Product Rule/Proof 1

Let $D$ be an open subset of the set of complex numbers.
Let $f, g: D \to \C$ be complex-differentiable functions on $D$
Let $f g$ denote the pointwise product of the functions $f$ and $g$.
Then $f g$ is complex-differentiable in $D$, and its derivative $\paren {f g}'$ is defined by:
:$\map {\paren {f g}'} z = \map {f'} z \map g z + \map f z \map {g'} z$
for all $z \in D$.

Proof:
Define $k: D \to \C$ as the pointwise product of $f$ and $g$, so $k = fg$.
Let $z_0 \in D$ be a point in $D$.
{{begin-eqn}}
{{eqn | l = \map {k'} {z_0}
      | r = \lim_{h \mathop \to 0} \frac {\map k {z_0 + h} - \map k {z_0} } h
      | c =
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map f {z_0 + h} \, \map g {z_0 + h} - \map f {z_0} \, \map g {z_0} } h
      | c =
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map f {z_0 + h} \, \map g {z_0 + h} - \map f {z_0 + h} \, \map g {z_0} + \map f {z_0 + h} \, \map g {z_0} - \map f {z_0} \, \map g {z_0} } h
      | c =
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\map f {z_0 + h} \frac {\map g {z_0 + h} - \map g {z_0} } h + \frac {\map f {z_0 + h} - \map f {z_0} } h \, \map g {z_0} }
      | c =
}}
{{eqn | r = \map f {z_0} \, \map {g'} {z_0} + \map {f'} {z_0} \, \map g {z_0}
      | c =
}}
{{eqn | ll= \leadsto
      | q = \forall z \in D
      | l = \map {k'} z
      | r = \map f z \, \map {g'} z + \map {f'} z \, \map g z
      | c = {{Defof|Derivative of Complex Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Combination Theorem for Complex Derivatives/Product Rule/Proof 2

Let $D$ be an open subset of the set of complex numbers.
Let $f, g: D \to \C$ be complex-differentiable functions on $D$
Let $f g$ denote the pointwise product of the functions $f$ and $g$.
Then $f g$ is complex-differentiable in $D$, and its derivative $\paren {f g}'$ is defined by:
:$\map {\paren {f g}'} z = \map {f'} z \map g z + \map f z \map {g'} z$
for all $z \in D$.

Proof:
Denote the open ball of $0$ by radius $r \in \R_{>0}$ as $\map {B_r} 0$.
Let $z \in D$.
By the Epsilon-Function Complex Differentiability Condition, it follows that there exists $r \in \R_{>0}$ such that for all $h \in \map {B_r} 0 \setminus \set 0$:
:$\map f {z + h} = \map f z + \map h {\map {f'} z + \map {\epsilon_f} h}$
:$\map g {z + h} = \map g z + \map h {\map {g'} z + \map {\epsilon_g} h}$
where $\epsilon_f, \epsilon_g: \map {B_r} 0 \setminus \set 0 \to \C$ are complex functions that converge to $0$ as $h$ tends to $0$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {f g} } {z + h}
      | r = \map f z \map g z + \map h {\map f z \map {g'} z + \map f z \map {\epsilon_g} h} + h \paren {\map g z \map {f'} z + \map g z \map {\epsilon_f} h} + {h^2} \paren {\map {f'} z + \map {\epsilon_f} h} \paren {\map {g'} z + \map {\epsilon_g} h}
}}
{{eqn | r = \map {\paren {f g} } z + h \paren {\map {f'} z \map g z + \map f z \map {g'} z + h \paren {\map {f'} z + \map {\epsilon_f} h} \paren {\map {g'} z + \map {\epsilon_g} h} }
}}
{{end-eqn}}
Define $\epsilon: \map {B_r} 0 \setminus \set 0 \to \C$ by:
:$\map \epsilon h = h \paren {\map {f'} z + \map {\epsilon_f} h} \paren {\map {g'} z + \map {\epsilon_g} h}$
From Product Rule for Limits of Complex Functions and Combined Sum Rule for Limits of Complex Functions:
:$\ds \lim_{h \mathop \to 0} \map \epsilon h = \paren {\lim_{h \mathop \to 0} h} \paren {\lim_{h \mathop \to 0} \paren {\map {f'} z + \map {\epsilon_f} h} } \paren {\lim_{h \mathop \to 0} \paren {\map {g'} z + \map {\epsilon_g} h} } = 0$
Then the Epsilon-Function Complex Differentiability Condition shows that:
:$\map {\paren {f g}'} z = \map {f'} z \map g z + \map f z \map {g'} z$
{{qed}}