avewright/proofwiki-math huggingface dataset:
Theorem: Partial Derivatives of tan^2 (x^2 - y^2)

Let:
:$\map f {x, y} = \map {\tan^2} {x^2 - y^2}$
Then:
{{begin-eqn}}
{{eqn | l = \map {f_1} {x, y}
      | r = 4 x \map \tan {x^2 - y^2} \map {\sec^2} {x^2 - y^2}
}}
{{eqn | l = \map {f_2} {1, 2}
      | r = 8 \tan 3 \sec^2 3
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map {f_1} {x, y}
      | r = \dfrac \partial {\partial x} {\map {\tan^2} {x^2 - y^2} }
      | c = {{Defof|Partial Derivative}}
}}
{{eqn | r = 2 \map \tan {x^2 - y^2} \map {\sec^2} {x^2 - y^2} \cdot 2 x
      | c = Derivative of Square of Tangent, Derivative of Square Function, Chain Rule for Derivatives
}}
{{eqn | r = 4 x \map \tan {x^2 - y^2} \map {\sec^2} {x^2 - y^2}
      | c = simplifying
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \map {f_2} {x, y}
      | r = \dfrac \partial {\partial y} {\map {\tan^2} {x^2 - y^2} }
      | c = {{Defof|Partial Derivative}}
}}
{{eqn | r = 2 \map \tan {x^2 - y^2} \map {\sec^2} {x^2 - y^2} \cdot \paren {-2 y}
      | c = Derivative of Square of Tangent, Derivative of Square Function, Chain Rule for Derivatives
}}
{{eqn | r = -4 y \map \tan {x^2 - y^2} \map {\sec^2} {x^2 - y^2}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \map {f_2} {1, 2}
      | r = -4 \paren 2 \map \tan {1^2 - 2^2} \map {\sec^2} {1^2 - 2^2}
      | c = 
}}
{{eqn | r = -8 \map \tan {-3} \map {\sec^2} {-3}
      | c = 
}}
{{eqn | r = -8 \paren {-\tan 3} \sec^2 3
      | c = Tangent Function is Odd, Secant Function is Even
}}
{{eqn | r = 8 \tan 3 \sec^2 3
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Square of Tangent

:$\map {\dfrac \d {\d x} } {\tan^2 x} = 2 \tan x \sec^2 x$
when $\cos x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\tan^2 x}
      | r = 2 \tan x \map {\dfrac \d {\d x} } {\tan x}
      | c = Chain Rule for Derivatives, Derivative of Square Function
}}
{{eqn | r = 2 \tan x \sec^2 x 
      | c = Derivative of Tangent Function
}}
{{end-eqn}}
{{qed}}
Category:Tangent Function
nr7j1qx0qa2pkgzchptcsv4cp87ohvw
Theorem: Partial Derivative wrt z of z^2 equals x^2 - 2 x y - 1 at (1, -2, -2)

Let $z^2 = x^2 - 2 x y - 1$.
Then:
:$\valueat {\dfrac {\partial z} {\partial x} } {x \mathop = 1, y \mathop = -2, z \mathop = -2} = -\dfrac 3 2$

Proof:
First we make sure that $\tuple {1, -2, -2}$ actually satisfies the equation:
{{begin-eqn}}
{{eqn | l = x^2 - 2 x y - 1
      | r = \paren 1^2 - 2 \paren 1 \paren {-2} - 1
      | c = at $\tuple {1, -2, -2}$
}}
{{eqn | r = 1 + 4 - 1
      | c = 
}}
{{eqn | r = 4
      | c = 
}}
{{eqn | r = \paren {-2}^2
      | c = 
}}
{{eqn | r = z^2
      | c = at $\tuple {1, -2, -2}$
}}
{{end-eqn}}
and it is seen that this is the case.
{{qed|lemma}}
Theorem: Partial Derivative/Examples/u - v + 2 w, 2 u + v + 2 w, u - v + w

Let:
{{begin-eqn}}
{{eqn | l = u - v + 2 w
      | r = x + 2 z
}}
{{eqn | l = 2 u + v - 2 w
      | r = 2 x - 2 z
}}
{{eqn | l = u - v + w
      | r = z - y
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial u} {\partial y}
      | r = 0
}}
{{eqn | l = \dfrac {\partial v} {\partial y}
      | r = 2
}}
{{eqn | l = \dfrac {\partial w} {\partial y}
      | r = 1
}}
{{end-eqn}}

Proof:
Partial differentiation {{WRT|Differentiation}} $y$ gives:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial u} {\partial y} - \dfrac {\partial v} {\partial y} + 2 \dfrac {\partial w} {\partial y}
      | r = 0
}}
{{eqn | l = 2 \dfrac {\partial u} {\partial y} + \dfrac {\partial v} {\partial y} - 2 \dfrac {\partial w} {\partial y}
      | r = 0
}}
{{eqn | l = \dfrac {\partial u} {\partial y} - \dfrac {\partial v} {\partial y} + \dfrac {\partial w} {\partial y}
      | r = -1
}}
{{end-eqn}}
which can be expressed in matrix form as:
:$\begin {pmatrix} 1 & -1 & 2 \\ 2 & 1 & -2 \\ 1 & -1 & 1 \end {pmatrix} \begin {pmatrix} \dfrac {\partial u} {\partial y} \\ \dfrac {\partial v} {\partial y} \\ \dfrac {\partial w} {\partial y} \end {pmatrix} = \begin {pmatrix} 0 \\ 0 \\ -1 \end {pmatrix}$
Solving by Cramer's Rule:
{{explain|Actually this is not Cramer's Rule, this will need to be taken care of}}
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {\begin {array} {ccc {{|}} c} 1 & -1 & 2 & 0 \\ 2 & 1 & -2 & 0 \\ 1 & -1 & 1 & -1 \end {array} }
      | c = 
}}
{{eqn | ll= \leadsto
      | o = 
      | r = \paren {\begin {array} {ccc {{|}} c} 1 & -1 & 2 & 0 \\ 0 & 3 & -6 & 0 \\ 0 & 0 & -1 & -1 \end {array} }
      | c = $\text r 2 \to \text r 2 - 2 \text r 1$, $\text r 3 \to \text r 3 - \text r 1$
}}
{{eqn | ll= \leadsto
      | o = 
      | r = \paren {\begin {array} {ccc {{|}} c} 1 & -1 & 2 & 0 \\ 0 & 1 & -2 & 0 \\ 0 & 0 & 1 & 1 \end {array} }
      | c = $\text r 2 \to \text r 2 / 3$, $\text r 3 \to -\text r 3$
}}
{{eqn | ll= \leadsto
      | o = 
      | r = \paren {\begin {array} {ccc {{|}} c} 1 & 0 & 0 & 0 \\ 0 & 1 & -2 & 0 \\ 0 & 0 & 1 & 1 \end {array} }
      | c = $\text r 1 \to \text r 1 - \text r 2$
}}
{{eqn | ll= \leadsto
      | o = 
      | r = \paren {\begin {array} {ccc {{|}} c} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 2 \\ 0 & 0 & 1 & 1 \end {array} }
      | c = $\text r 2 \to \text r 2 + 2 \text r 3$
}}
{{end-eqn}}
The solution can be read directly:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial u} {\partial y}
      | r = 0
}}
{{eqn | l = \dfrac {\partial v} {\partial y}
      | r = 2
}}
{{eqn | l = \dfrac {\partial w} {\partial y}
      | r = 1
}}
{{end-eqn}}
{{qed}}
Theorem: Partial Derivatives of x tan^-1 (x^2 + y)

Let:
:$\map f {x, y} = x \map \arctan {x^2 + y}$
Then:
{{begin-eqn}}
{{eqn | l = \map {f_1} {1, 0}
      | r = \dfrac \pi 4 + 1
}}
{{eqn | l = \map {f_2} {x, y}
      | r = \dfrac x {1 + \paren {x^2 + y}^2}
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map {f_1} {x, y}
      | r = \map {\dfrac \partial {\partial x} } {x \map \arctan {x^2 + y} }
      | c = {{Defof|Partial Derivative}}
}}
{{eqn | r = \map \arctan {x^2 + y} \map {\dfrac \partial {\partial x} } x + x \map {\dfrac \partial {\partial x} } {\map \arctan {x^2 + y} }
      | c = Product Rule for Derivatives
}}
{{eqn | r = \map \arctan {x^2 + y} + x \cdot \dfrac 1 {1 + \paren {x^2 + y}^2} \cdot 2 x
      | c = Product Rule for Derivatives, Derivative of Arctangent Function, Chain Rule for Derivatives
}}
{{eqn | r = \map \arctan {x^2 + y} + \dfrac {2 x^2} {1 + \paren {x^2 + y}^2}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \map {f_1} {1, 0}
      | r = \map \arctan {1^2 + 0} + \dfrac {2 \times 1^2} {1 + \paren {1^2 + 0}^2}
      | c = substituting $x = 1$ and $y = 0$
}}
{{eqn | r = \map \arctan 1 + \dfrac 2 2
      | c = simplifying
}}
{{eqn | r = \dfrac \pi 4 + 1
      | c = Tangent of $45 \degrees$
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \map {f_2} {x, y}
      | r = \map {\dfrac \partial {\partial y} } {x \map \arctan {x^2 + y} }
      | c = {{Defof|Partial Derivative}}
}}
{{eqn | r = x \dfrac 1 {1 + \paren {x^2 + y}^2} \cdot 1
      | c = Derivative of Identity Function, Derivative of Arctangent Function, Chain Rule for Derivatives
}}
{{eqn | r = \dfrac x {1 + \paren {x^2 + y}^2}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Partial Derivatives of x ln y^2 + y e^z

Let:
:$\map f {x, y, z} = x \ln y^2 + y e^z$
Then:
{{begin-eqn}}
{{eqn | l = \map {f_1} {1, -1, 0}
      | r = 0
}}
{{eqn | l = \map {f_2} {x, x y, y + z}
      | r = \dfrac 2 y + e^{y + z}
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map {f_1} {x, y, z}
      | r = \ln y^2
      | c = Derivative of Constant Multiple, Derivative of Identity Function, holding $y$ and $z$ constant
}}
{{eqn | ll= \leadsto
      | l = \map {f_1} {1, -1, 0}
      | r = \map \ln {\paren {-1}^2}
      | c = substituting $\tuple {1, -1, 0}$ for $\tuple {x, y, z}$
}}
{{eqn | r = \ln 1
      | c = simplifying
}}
{{eqn | r = 0
      | c = Natural Logarithm of 1 is 0
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \map {f_2} {x, y, z}
      | r = \map {\dfrac \partial {\partial y} } {x \ln y^2 + y e^z}
      | c = {{Defof|Partial Derivative}}
}}
{{eqn | r = \dfrac x {y^2} \cdot 2 y + e^z
      | c = Derivative of Natural Logarithm, Power Rule for Derivatives, Chain Rule for Derivatives, holding $x$ and $z$ constant
}}
{{eqn | r = \dfrac {2 x} y + e^z
      | c = simplification
}}
{{eqn | ll= \leadsto
      | l = \map {f_2} {x, x y, y + z}
      | r = \dfrac {2 x} {x y} + e^{y + z}
      | c = substituting $\tuple {x, x y, y + z}$ for $\tuple {x, y, z}$
}}
{{eqn | r = \dfrac 2 y + e^{y + z}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Partial Derivatives of x^y^z

Let:
:$u = x^{\paren {y^z} }$
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial u} {\partial x}
      | r = y^z x^{\paren {y^z - 1} }
}}
{{eqn | l = \dfrac {\partial u} {\partial y}
      | r = x^{y^z} z y^{z - 1} \ln x
}}
{{eqn | l = \dfrac {\partial u} {\partial z}
      | r = x^{\paren {y^z} } y^z \ln x \ln y
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial u} {\partial x}
      | r = y^z x^{\paren {y^z - 1} }
      | c = Power Rule for Derivatives, keeping $y$ and $z$ constant
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = u
      | r = x^{\paren {y^z} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \ln u
      | r = \map \ln {x^{\paren {y^z} } }
      | c = 
}}
{{eqn | n = 1
      | r = y^z \ln x
      | c = Logarithm of Power
}}
{{eqn | ll= \leadsto
      | l = \frac 1 u \dfrac {\partial u} {\partial y}
      | r = z y^{z - 1} \ln x
      | c = Derivative of Natural Logarithm, Power Rule for Derivatives, Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial u} {\partial y}
      | r = u z y^{z - 1} \ln x
      | c = multiplying both sides by $u$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial u} {\partial y}
      | r = x^{\paren {y^z} } z y^{z - 1} \ln x
      | c = substituting for $u$
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \ln u
      | r = y^z \ln x
      | c = from $(1)$
}}
{{eqn | ll= \leadsto
      | l = \frac 1 u \dfrac {\partial u} {\partial z}
      | r = y^z \ln x \ln y
      | c = Derivative of Natural Logarithm, Derivative of General Exponential Function, Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial u} {\partial z}
      | r = u y^z \ln x \ln y
      | c = multiplying both sides by $u$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial u} {\partial z}
      | r = x^{\paren {y^z} } y^z \ln x \ln y
      | c = substituting for $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Partial Derivatives of x^u + u^y

Let:
:$u = x^u + u^y$
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial u} {\partial x}
      | r = \frac {u^2} {x \paren {1 - u \ln x - y} }
}}
{{eqn | l = \dfrac {\partial u} {\partial y}
      | r = \frac {u \ln u} {1 - u \ln x - y}
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = u
      | r = x^u + u^y
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \ln u
      | r = u \ln x + y \ln u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac 1 u \dfrac {\partial u} {\partial x}
      | r = \frac u x + \ln x \dfrac {\partial u} {\partial x} + \frac y u \dfrac {\partial u} {\partial x}
      | c = Derivative of Natural Logarithm, Chain Rule for Derivatives keeping $y$ constant
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial u} {\partial x} \paren {\frac 1 u - \ln x - \frac y u}
      | r = \frac u x
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial u} {\partial x} \paren {\frac {1 - u \ln x - y} u}
      | r = \frac u x
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial u} {\partial x}
      | r = \frac {u^2} {x \paren {1 - u \ln x - y} }
      | c = rearranging
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \ln u
      | r = u \ln x + y \ln u
      | c = from $(1)$
}}
{{eqn | ll= \leadsto
      | l = \frac 1 u \dfrac {\partial u} {\partial y}
      | r = \ln x \dfrac {\partial u} {\partial y} + \ln u + \frac y u \dfrac {\partial u} {\partial y}
      | c = Derivative of Natural Logarithm, Product Rule for Derivatives, Chain Rule for Derivatives keeping $x$ constant
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial u} {\partial y} \paren {\frac 1 u - \ln x - \frac y u}
      | r = \ln u
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial u} {\partial y} \paren {\frac {1 - u \ln x - y} u}
      | r = \ln u
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial u} {\partial y}
      | r = \frac {u \ln u} {1 - u \ln x - y}
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Partial Derivatives of u^2 + x^2 + y^2, u - v^3 + 3 x

Let:
{{begin-eqn}}
{{eqn | l = u^2 + x^2 + y^2
      | r = 3
}}
{{eqn | l = u - v^3 + 3 x
      | r = 4
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial u} {\partial x}
      | r = -\dfrac x u
}}
{{eqn | l = \dfrac {\partial u} {\partial y}
      | r = -\dfrac y u
}}
{{eqn | l = \dfrac {\partial v} {\partial x}
      | r = \dfrac {x - 3 u} {3 u v^2}
}}
{{eqn | l = \dfrac {\partial v} {\partial y}
      | r = \dfrac y {3 u v^2}
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = 2 u \dfrac {\partial u} {\partial x} + 2 x
      | r = 0
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \dfrac {\partial u} {\partial x}
      | r = -\dfrac x u
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = 2 u \dfrac {\partial u} {\partial y} + 2 y
      | r = 0
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \dfrac {\partial u} {\partial y}
      | r = -\dfrac y u
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \dfrac {\partial u} {\partial x} + 3 v^2 \dfrac {\partial v} {\partial x} + 3
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -\dfrac x u + 3 v^2 \dfrac {\partial v} {\partial x} + 3
      | r = 0
      | c = substituting for $\dfrac {\partial u} {\partial x}$ from $(1)$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial v} {\partial x}
      | r = \dfrac {x - 3 u} {3 u v^2}
      | c = rearranging
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \dfrac {\partial u} {\partial y} + 3 v^2 \dfrac {\partial v} {\partial y}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -\dfrac y u + 3 v^2 \dfrac {\partial v} {\partial x}
      | r = 0
      | c = substituting for $\dfrac {\partial u} {\partial y}$ from $(2)$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\partial v} {\partial y}
      | r = \dfrac y {3 u v^2}
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Number of Terms in Homogeneous Polynomial

The number of terms in a homogeneous polynomial of degree $n$ in $m$ indeterminates is given by:
:$N = \dbinom {n + m - 1} n = \dfrac {\paren {n + m - 1}!}{n! \, \paren {m - 1}!}$

Proof:
{{ProofWanted|By induction, probably, but really need to rationalise the existing material on polynomials}}
Theorem: Heine-Borel Theorem/Normed Vector Space/Necessary Condition

Let $\struct {X, \norm {\, \cdot \,} }$ be a finite-dimensional normed vector space.
Let $K \subseteq X$ be closed and bounded.
Then $K$ is a compact subset.

Proof:
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $K$.
$\sequence {x_n}_{n \mathop \in \N}$ is bounded.
We have that bounded sequence in finite-dimensional space has a convergent subsequence.
Hence, $\sequence {x_n}_{n \mathop \in \N}$ has a convergent subsequence $\sequence {x_{n_k} }_{k \mathop \in \N}$.
Denote the limit $\ds \lim_{k \mathop \to \infty} \sequence {x_{n_k} } = L$.
By assumption, $K$ is closed.
By equivalence of definitions, $L \in K$.
By definition, $K$ is compact.
Theorem: Compact Subset of Normed Vector Space is Closed and Bounded

Let $\struct {X, \norm {\,\cdot\,}}$ be a normed vector space.
Let $K \subset X$ be a compact subset.
Then $K$ is closed and bounded.

Proof:
=== Closedness ===
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $K$.
Suppose, $\sequence {x_n}_{n \mathop \in \N}$ converges to $L \in K$. 
Then there is a subsequence $\sequence {x_{n_k}}_{k \mathop \in \N}$ convergent to $L' \in K$. 
But $\sequence {x_{n_k}}_{k \mathop \in \N}$ is a subsequence of $\sequence {x_n}_{n \mathop \in \N}$.
Hence, $\sequence {x_{n_k}}_{k \mathop \in \N}$ converges to $L$.
By uniqueness of limits, $L = L'$.
By definition, $K$ is closed.
=== Boundedness ===
Suppose, $K$ is not bounded.
Then:
:$\forall n \in \N : \exists x_n \in K: \norm {x_n} > n$
Therefore, no subsequence of $\sequence {x_n}_{n \mathop \in \N}$ is convergent.
Hence, $K$ is not compact.
This is in contradiction with the assumption.
Thus, $K$ is bounded.
Theorem: Sine of X over X is not Continuous at 0

Let $f$ be the real function defined as:
:$\map f x := \dfrac {\sin x} x$
Then $f$ is not continuous at $x = 0$.

Proof:
For $f$ to be continuous at $x = 0$ it is necessary that it be defined there.
But at the point $x = 0$, we have that $\map f x = \dfrac {\sin 0} 0$.
Division by $0$ is not defined.
Hence $f$ is not continuous at $x = 0$.
{{qed}}
Theorem: Reciprocal Function is Discontinuous at Zero

Let $f$ be the real function defined as:
:$\map f x = \dfrac 1 x$
for $x \ne 0$
Then $\map f x$ cannot be extended to a real function $g$ on $\R$ such that $\map g x$ is continuous on $\openint {-1} 1$.

Proof:
It is apparent that $f$ is itself not continuous at $x = 0$.
We need to show that whatever we define $\map g 0$ to be, $\ds \lim_{x \mathop \to 0} \map f x \ne \map f 0$.
Let $\map g 0 = c$.
Let $\epsilon$ be selected.
Let $x$ be chosen such that $x < \dfrac 1 c$.
Then $\dfrac 1 x > c$.
It follows that
:$\ds \lim_{x \mathop \to 0^+} \map f x > c$
and so:
$\ds \lim_{x \mathop \to 0} \map f x \ne \map f 0$
{{qed}}
Theorem: Right-Hand Derivative not Limit of Derivative from Right

Let $f$ be a real function.
Let the right-hand derivative $f'_+$ of $f$ exist.
Then it is not necessarily the case that:
:$\map {f'_+} a$
is the same thing as:
:$\map {f'} {a^+}$

Proof:
By definition:
:$\map {f'_+} a := \ds \lim_{h \mathop \to 0} \dfrac {\map f {a + h} - \map f a} h$
while:
:$\map {f'} {a^+} := \ds \lim_{x \mathop \to a^+} \map {f'} x$
Let:
:$\map f x = \begin {cases} x^2 \sin \dfrac 1 x & : x \ne 0 \\ 0 & : x = 0 \end {cases}$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f'_+} 0
      | r = \lim_{h \mathop \to 0} \dfrac {h^2 \sin \dfrac 1 h - 0} h
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} h \sin \dfrac 1 h
      | c = 
}}
{{eqn | r = 0
      | c = Limit of $x \sin \dfrac 1 x$ at $0$
}}
{{end-eqn}}
but:
{{begin-eqn}}
{{eqn | l = \map {f'} {0^+}
      | r = \lim_{x \mathop \to 0^+} \paren {2 x \sin \dfrac 1 x - \cos \dfrac 1 x}
      | c = which does not exist
}}
{{end-eqn}}
{{qed}}
Theorem: Function in Differentiability Class 1 is also in Continuity Class

Let $f$ be a real function. 
Let $f$ be an element of differentiability class $C^1$.
Then $f$ is also an element of the class $C$ of continuous real functions.

Proof:
By definition of $C^1$, $f \in C^1$ {{iff}} $f$ is differentiable.
By definition of $C$, $f \in C$ {{iff}} $f$ is continuous.
The result follows from Differentiable Function is Continuous.
{{qed}}
Theorem: Differentiability Class is Subset of Differentiability Class of Lower Order

Let $f$ be a real function. 
Let $f$ be an element of differentiability class $C^n$.
Then:
:$\forall k \in \set {0, 1, \ldots, n - 1}: f \in C^k$
That is, $f$ is in all differentiability classes of order less than $n$.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 1}$, let $\map P n$ be the proposition:
:$f \in C^n \implies \forall k \in \set {0, 1, \ldots, n - 1}: f \in C^k$
Theorem: Niven's Theorem/Lemma

For any integer $n \ge 1$, there exists a polynomial $\map {F_n} x$ such that:
:$\map {F_n} {2 \cos t} = 2 \cos n t$
In addition:
:$\deg F_n = n$
and $F_n$ is a monic polynomial with integer coefficients.

Proof:
The proof proceeds by induction.
For $n = 1$, it is seen that:
:$\map {F_1} x = x$
fulfils the propositions.
For $n = 2$:
:$\map {F_2} x = x^2 - 2$
For $n > 2$:
{{begin-eqn}}
{{eqn | l = 2 \map \cos {n - 1} t \cos t
      | r = \cos n t + \map \cos {n - 2} t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 \cos n t
      | r = \paren {2 \map \cos {n - 1} t} \paren {2 \cos t} - 2 \map \cos {n - 2} t
      | c = 
}}
{{eqn | r = 2 \cos t \map {F_{n - 1} } {2 \cos t} - \map {F_{n - 2} } {2 \cos t}
      | c = 
}}
{{end-eqn}}
so:
: $\map {F_n} x = x \map {F_{n - 1}} x - \map {F_{n - 2}} x \in \Z \sqbrk x$
will fulfil:
: $\map {F_n} {2 \cos t} = 2 \cos n t$
Because $\deg F_{n - 1} = n - 1$ and $\deg F_{n - 2} = n - 2$, we can conclude that:
:$\deg F_n = \deg \paren {x \map {F_{n - 1}} x - \map {F_{n - 2}} x} = n$
In addition, the leading coefficient of $F_n$ is equal to the leading coefficient of $F_{n - 1}$, which is $1$.
Hence the result.
{{qed}}
Category:Proofs by Induction
Category:Niven's Theorem
lztaoav0ncqzfhjbh4t0sfvel7bomv5
Theorem: Closed and Bounded Subset of Normed Vector Space is not necessarily Compact

Let $\struct {X, \norm {\,\cdot\,} }$ be a normed vector space.
Let $K \subset X$ be a closed and bounded subset.
Then $K$ is not necessarily compact.

Proof:
Let $\struct {\ell^2, \norm {\, \cdot \,}}_2$ be the 2-sequence space.
Let $K$ be a closed unit ball in $\struct {\ell^2, \norm {\, \cdot \,}}_2$:
:$K := \set {\mathbf x \in \ell^2 : \norm {\mathbf x}_2 \le 1}$
$K$ is bounded and closed.
Let $\sequence {\mathbf x_n}_{n \mathop \in \N}$ be a sequence such that:
:$\mathbf x_n := \tuple {0, \ldots 0, 1, 0, \ldots}$
where $1$ is in the $n$-th component of $\mathbf x_n$.
Then:
:$\forall n \in \N : \mathbf x_n \in K \subset \ell^2$
However:
:$\forall n, m \in \N : n \ne m : \norm {\mathbf x_n - \mathbf x_m}_2 = \sqrt 2$
In other words, $\sequence {\mathbf x_n}$ is not a Cauchy sequence.
By Convergent Subsequence of Cauchy Sequence, $\sequence {\mathbf x_n}$ has no convergent subsequence.
Therefore, a closed and bounded space $K$ has a sequence $\sequence {\mathbf x_n}_{n \mathop \in \N}$ which contains a non-convergent subsequence.
{{qed}}
Theorem: Closed and Bounded Subset of Normed Vector Space is not necessarily Compact

Let $\struct {X, \norm {\,\cdot\,} }$ be a normed vector space.
Let $K \subset X$ be a closed and bounded subset.
Then $K$ is not necessarily compact.

Proof:
Let $\struct {\CC \closedint 0 1, \norm {\, \cdot \,}_\infty}$ be the normed vector space of continuous on closed interval real-valued functions with supremum norm.
Consider a closed unit ball with the center at $0$ at $\struct {\CC, \norm {\, \cdot \,}_\infty}$:
:$K := \set {x \in \CC \closedint 0 1 : \norm x_\infty \le 1}$.
We have that $K$ is bounded and closed.
Consider the following sequence of graphs:
:<nowiki>$\map {x_n} t = \begin{cases}
2^{n + 2} t & : \ds \sum_{i \mathop = 1}^n \frac 1 {2^i} \le t < \sum_{i \mathop = 1}^n \frac 1 {2^i} + \frac 1 {2^{n + 2}}  \\
\ds 1 - 2^{n + 2} \paren {t - \paren {\sum_{i \mathop = 1}^n \frac 1 {2^i} + \frac 1 {2^{n + 2}}}} & : \ds \sum_{i \mathop = 1}^n \frac 1 {2^i} + \frac 1 {2^{n + 2}} \le t \le \sum_{i \mathop = 1}^{n + 1} \frac 1 {2^i} \\
0 & : \text {otherwise}
\end{cases}$</nowiki>
where $n \in \N$.
We have that:
:$\forall n, m \in \N : n \ne m \implies \norm {x_n - x_m}_\infty = 1$
Hence, $\sequence {x_n}_{n \mathop \in \N}$ is not a Cauchy sequence.
We have that every convergent sequence is a Cauchy sequence.
Hence, $\sequence {x_n}_{n \mathop \in \N}$ is not convergent.
Therefore, any subsequence of $\sequence {x_n}_{n \mathop \in \N}$ is also divergent.
Thus, a closed unit ball, which is closed and bounded, is not compact in $\struct {\CC \closedint 0 1, \norm {\, \cdot \,}_\infty}$.
{{qed}}
Theorem: Floor Function is Continuous on Right at Integer

Let $f$ be the real function defined as:
:$\map f x = \floor x$
where $\floor{\, \cdot \,}$ denotes the floor function.
Let $n \in \Z$ be an integer.
Then $\map f x$ is continuous on the right at $n$.

Proof:
From Real Number is Integer iff equals Floor:
:$\floor n = n$
By definition $\floor x$ is the unique integer such that:
:$\floor x \le x < \floor x + 1$
Consider the open real interval:
:$\II = \openint n {n + 1}$
By definition of $\floor x$ we have that:
:$\forall x \in \II: \floor x = n$
That is:
:$\forall x \in \II: \floor x - n = 0$
Let $\epsilon \in \R_{>0}$.
Let $\delta \in \openint n {n + 1}$.
Then:
:$\forall x \in \II: n < x < n + \delta: \size {\floor x - n} < \epsilon$
That is:
:$\ds \lim_{x \mathop \to n^+} \floor x = \floor n$
Hence, by definition, $\map f x$ is continuous on the right at $n$.
{{qed}}