PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Matrix differentials obey the sum rule, product rule, and adjoint rule

Statement

In the real Fr'echet sense on matrix spaces:

$D (A \mapsto A + B) (A) [H] = H$ for fixed $B$ ;
$D (A, B \mapsto A B) (A, B) [H, K] = H B + A K$ ;
$D (A \mapsto A^{*}) (A) [H] = H^{*}$ .

Equivalently, differential notation gives $d (A + B) = d A + d B$ , $d (A B) = d A B + A d B$ , and $d (A^{*}) = (d A)^{*}$ .

Facts & Assumptions

Given: Compatible matrices and perturbation directions.

[F1]

Real Fr'echet differentiability means $F (A + H) = F (A) + D F (A) [H] + o (∥ H ∥_{F})$ (The real Frechet derivative on real and complex matrix spaces with the Frobenius norm).

Proof

technique · direct

1.1

For the sum map, $(A + H) + B = (A + B) + H$ , so the linear term is already $H$ . For the adjoint map, $(A + H)^{*} = A^{*} + H^{*}$ , so the linear term is $H^{*}$ . Both have zero remainder in the sense of [F1].

F1algebra

2.1

For the product map, $(A + H) (B + K) = A B + H B + A K + H K .$ The bilinear term $H K$ satisfies $∥ H K ∥_{F} \leq ∥ H ∥_{F} ∥ K ∥_{F} = o (∥ (H, K) ∥)$ , so [F1] identifies the derivative as $(H, K) \mapsto H B + A K$ . This is exactly the product rule.

F1algebra∎

Depends on

Used by

Matrix quadratic forms have the expected first derivative and Hessian Proposition
On the invertible locus, Dinv(A)[H]=-A⁻¹HA⁻¹ Theorem

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Alan Edelman and Steven G. Johnson, Matrix Calculus for Machine Learning and Beyond (standard reference, not scraped)