ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4912 on D111: Euclidean real function derivative
Subresult of R4913: Strong derivative for euclidean real quadratic form without translation
Strong derivative for symmetric euclidean real quadratic form
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}
(ii) \begin{equation} A^T = A \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) = 2 (A x_0 )^T x \end{equation}
Then $L$ is a D5681: Real function derivative for $f$ at $x_0$.
Subresults
▶ R4909: Derivative for euclidean real self-dot product function
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}
(ii) \begin{equation} A^T = A \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) = 2 (A x_0 )^T x \end{equation}