ThmDex – An index of mathematical definitions, results, and conjectures.

Result R4909 on D111: Euclidean real function derivative
Subresult of R4912: Strong derivative for symmetric euclidean real quadratic form

Derivative for euclidean real self-dot product function

Formulation 0

Let $f : \mathbb{R}^{N \times 1} \to \mathbb{R}$ be a D4364: Real function such that

(i)	\begin{equation} f(x) = x^T x \end{equation}

Let $L : \mathbb{R}^{N \times 1} \to \mathbb{R}$ be a D4364: Real function such that

(i)	$x_0 \in \mathbb{R}^{N \times 1}$ is a D5200: Real column matrix
(ii)	\begin{equation} L(x) = 2 x^T_0 x \end{equation}

Then $L$ is a D5681: Real function derivative for $f$ at $x_0$.

Formulation 1

Let $f : \mathbb{R}^{N \times 1} \to \mathbb{R}$ be a D4364: Real function such that

(i)	\begin{equation} f(x) = \Vert x \Vert^2_2 \end{equation}

Let $L : \mathbb{R}^{N \times 1} \to \mathbb{R}$ be a D4364: Real function such that

(i)	$x_0 \in \mathbb{R}^{N \times 1}$ is a D5200: Real column matrix
(ii)	\begin{equation} L(x) = 2 x^T_0 x \end{equation}

Then $L$ is a D5681: Real function derivative for $f$ at $x_0$.

Subresults

▶	R5537: Derivative function for euclidean real self-dot product function

Proofs

Proof 0

Let $f : \mathbb{R}^{N \times 1} \to \mathbb{R}$ be a D4364: Real function such that

(i)	\begin{equation} f(x) = x^T x \end{equation}

Let $L : \mathbb{R}^{N \times 1} \to \mathbb{R}$ be a D4364: Real function such that

(i)	$x_0 \in \mathbb{R}^{N \times 1}$ is a D5200: Real column matrix
(ii)	\begin{equation} L(x) = 2 x^T_0 x \end{equation}

This result is a particular case of R4912: Strong derivative for symmetric euclidean real quadratic form where $A$ is an identity matrix. $\square$