ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4913 on D111: Euclidean real function derivative
Subresult of R4960: Strong derivative for euclidean real quadratic form
Strong derivative for euclidean real quadratic form without translation
Formulation 0
Let $f : \mathbb{R}^{N \times 1} \to \mathbb{R}$ be a D4364: Real function such that
(i) \begin{equation} \exists \, A \in \mathbb{R}^{N \times N} : \forall \, x \in \mathbb{R}^{N \times 1} : f(x) = x^T A 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} \forall \, x \in \mathbb{R}^{N \times 1} : L(x) = (A x_0 + A^T x_0)^T x \end{equation}
Then $L$ is a D5681: Real function derivative for $f$ at $x_0$.
Subresults
▶ R4912: Strong derivative for symmetric euclidean real quadratic form
Proofs
Proof 1
Let $f : \mathbb{R}^{N \times 1} \to \mathbb{R}$ be a D4364: Real function such that
(i) \begin{equation} \exists \, A \in \mathbb{R}^{N \times N} : \forall \, x \in \mathbb{R}^{N \times 1} : f(x) = x^T A 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} \forall \, x \in \mathbb{R}^{N \times 1} : L(x) = (A x_0 + A^T x_0)^T x \end{equation}
This result is a particular case of R4960: Strong derivative for euclidean real quadratic form. $\square$