M03 — Shared-path chain rule

{"text": "{\n "readback": "Theorem M03_chain_rule_pair (in namespace VathekProof). For all natural numbers $d$ and $m$ (either of which may be $0$), write $E_d$ and $E_m$ for the Euclidean spaces of real $d$- and $m$-tuples, equipped with the standard inner product $\\\\langle u, v\\\\rangle = \\\\sum_j u_j v_j$ (sum over the $d$, resp. $m$, coordinates) and the norm $\\\\|u\\\\| = \\\\sqrt{\\\\sum_j u_j^2}$. The theorem takes as data, each of them arbitrary except as constrained by the four hypotheses below: a function $f : E_d \\\\times E_m \\\\to \\\\mathbb{R}$ (the product space is normed by $\\\\|(w, v)\\\\| = \\\\max\\\\{\\\\|w\\\\|, \\\\|v\\\\|\\\\}$); a function $h : E_d \\\\to E_m$; a point $w_0 \\\\in E_d$; vectors $a \\\\in E_d$ and $c \\\\in E_m$; and a continuous $\\\\mathbb{R}$-linear map $h' : E_d \\\\to E_m$ (in finite dimensions continuity is automatic, so $h'$ is simply a linear map, represented in the standard bases by an $m \\\\times d$ real matrix $M$).\n\nThroughout, \u201cgradient\u201d is meant in the inner-product (Riesz) sense. For a real-valued function $\\\\varphi$ on a Euclidean space, the assertion \u201c$\\\\varphi$ has gradient $g$ at the point $x$\u201d means that $\\\\varphi$ is Fr\u00e9chet differentiable at $x$ and its derivative functional is exactly the map $z \\\\mapsto \\\\langle g, z\\\\rangle$; equivalently,\n\n

\n\nIn particular the assertion includes the existence of the Fr\u00e9chet derivative, and the representing vector $g$ is unique when it exists.\n\nThe four hypotheses are:\n\n- $(\\\\mathrm{ha})$ the function $w \\\\mapsto f(w,\\\\, h(w_0))$ \u2014 that is, $f$ with its second argument frozen at the single value $h(w_0)$ \u2014 has gradient $a$ at the point $w_0$;\n- $(\\\\mathrm{hc})$ the function $v \\\\mapsto f(w_0,\\\\, v)$ \u2014 $f$ with its first argument frozen at $w_0$ \u2014 has gradient $c$ at the point $v = h(w_0)$;\n- $(\\\\mathrm{hh})$ $h$ is Fr\u00e9chet differentiable at $w_0$ with derivative $h'$, i.e. $h(w_0 + z) = h(w_0) + h'(z) + o(\\\\|z\\\\|)$ as $z \\\\to 0$;\n- $(\\\\mathrm{hf})$ $f$, regarded as a function of the pair $(w, v)$, is Fr\u00e9chet differentiable at the single point $(w_0,\\\\, h(w_0))$ \u2014 existence only, with no derivative value specified.\n\nNote exactly where the evaluations sit: both partial-gradient hypotheses and the differentiability hypothesis $(\\\\mathrm{hf})$ concern the one common pair $(w_0, h(w_0))$ \u2014 $(\\\\mathrm{ha})$ varies the first coordinate around $w_0$ while the second is held at $h(w_0)$, and $(\\\\mathrm{hc})$ varies the second coordinate around $h(w_0)$ while the first is held at $w_0$; $(\\\\mathrm{hh})$ is taken at $w_0$.\n\nThe conclusion asserts that the composite function $w \\\\mapsto f(w,\\\\, h(w))$ has gradient\n\n

\n\nat $w_0$; that is, this composite is Fr\u00e9chet differentiable at $w_0$ and its derivative there is the functional z \\\\mapsto \\\\langle a + h'^\\\\dagger c,\\\\; z\\\\rangle. Here h'^\\\\dagger denotes the adjoint of $h'$: the unique continuous linear map h'^\\\\dagger : E_m \\\\to E_d characterized by\n\n

\n\nIn matrix terms, if $h'$ is given by the $m \\\\times d$ matrix $M$, then h'^\\\\dagger is given by the transpose $M^{\\\\mathsf T} \\\\in \\\\mathbb{R}^{d \\\\times m}$, so the claimed gradient vector is $a + M^{\\\\mathsf T} c$.\n\nEverything in the statement is pointwise: $f$ and $h$ are not required to be continuous, differentiable, or bounded anywhere except as stated at the points $w_0$, $h(w_0)$, and $(w_0, h(w_0))$, and the conclusion likewise concerns only the single point $w_0$. Degenerate dimensions are included in the quantifiers: if $m = 0$, then $E_m$ is the one-point zero space, $c$ and $h(w_0)$ are necessarily its unique element $0$, $h'$ is the unique (zero) map and h'^\\\\dagger c = 0, $h$ is constant, and the conclusion coincides verbatim with hypothesis $(\\\\mathrm{ha})$; if $d = 0$ the parameter space $E_d$ is a single point and the gradient assertion becomes trivial in content. The hypotheses are jointly satisfiable \u2014 for example $f(w, v) = \\\\langle p, w\\\\rangle + \\\\langle q, v\\\\rangle$ with an affine $h$ and any $w_0$ satisfies all four, with $a = p$, $c = q$, and $h'$ the linear part \u2014 so the statement is not vacuous."\n}", "details": {"resolvedPath": "/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB-M03.md", "contentType": "text/markdown", "totalLines": 3, "displayContent": {"text": "{\n "readback": "Theorem M03_chain_rule_pair (in namespace VathekProof). For all natural numbers $d$ and $m$ (either of which may be $0$), write $E_d$ and $E_m$ for the Euclidean spaces of real $d$- and $m$-tuples, equipped with the standard inner product $\\\\langle u, v\\\\rangle = \\\\sum_j u_j v_j$ (sum over the $d$, resp. $m$, coordinates) and the norm $\\\\|u\\\\| = \\\\sqrt{\\\\sum_j u_j^2}$. The theorem takes as data, each of them arbitrary except as constrained by the four hypotheses below: a function $f : E_d \\\\times E_m \\\\to \\\\mathbb{R}$ (the product space is normed by $\\\\|(w, v)\\\\| = \\\\max\\\\{\\\\|w\\\\|, \\\\|v\\\\|\\\\}$); a function $h : E_d \\\\to E_m$; a point $w_0 \\\\in E_d$; vectors $a \\\\in E_d$ and $c \\\\in E_m$; and a continuous $\\\\mathbb{R}$-linear map $h' : E_d \\\\to E_m$ (in finite dimensions continuity is automatic, so $h'$ is simply a linear map, represented in the standard bases by an $m \\\\times d$ real matrix $M$).\n\nThroughout, \u201cgradient\u201d is meant in the inner-product (Riesz) sense. For a real-valued function $\\\\varphi$ on a Euclidean space, the assertion \u201c$\\\\varphi$ has gradient $g$ at the point $x$\u201d means that $\\\\varphi$ is Fr\u00e9chet differentiable at $x$ and its derivative functional is exactly the map $z \\\\mapsto \\\\langle g, z\\\\rangle$; equivalently,\n\n

\n\nIn particular the assertion includes the existence of the Fr\u00e9chet derivative, and the representing vector $g$ is unique when it exists.\n\nThe four hypotheses are:\n\n- $(\\\\mathrm{ha})$ the function $w \\\\mapsto f(w,\\\\, h(w_0))$ \u2014 that is, $f$ with its second argument frozen at the single value $h(w_0)$ \u2014 has gradient $a$ at the point $w_0$;\n- $(\\\\mathrm{hc})$ the function $v \\\\mapsto f(w_0,\\\\, v)$ \u2014 $f$ with its first argument frozen at $w_0$ \u2014 has gradient $c$ at the point $v = h(w_0)$;\n- $(\\\\mathrm{hh})$ $h$ is Fr\u00e9chet differentiable at $w_0$ with derivative $h'$, i.e. $h(w_0 + z) = h(w_0) + h'(z) + o(\\\\|z\\\\|)$ as $z \\\\to 0$;\n- $(\\\\mathrm{hf})$ $f$, regarded as a function of the pair $(w, v)$, is Fr\u00e9chet differentiable at the single point $(w_0,\\\\, h(w_0))$ \u2014 existence only, with no derivative value specified.\n\nNote exactly where the evaluations sit: both partial-gradient hypotheses and the differentiability hypothesis $(\\\\mathrm{hf})$ concern the one common pair $(w_0, h(w_0))$ \u2014 $(\\\\mathrm{ha})$ varies the first coordinate around $w_0$ while the second is held at $h(w_0)$, and $(\\\\mathrm{hc})$ varies the second coordinate around $h(w_0)$ while the first is held at $w_0$; $(\\\\mathrm{hh})$ is taken at $w_0$.\n\nThe conclusion asserts that the composite function $w \\\\mapsto f(w,\\\\, h(w))$ has gradient\n\n

\n\nat $w_0$; that is, this composite is Fr\u00e9chet differentiable at $w_0$ and its derivative there is the functional z \\\\mapsto \\\\langle a + h'^\\\\dagger c,\\\\; z\\\\rangle. Here h'^\\\\dagger denotes the adjoint of $h'$: the unique continuous linear map h'^\\\\dagger : E_m \\\\to E_d characterized by\n\n

\n\nIn matrix terms, if $h'$ is given by the $m \\\\times d$ matrix $M$, then h'^\\\\dagger is given by the transpose $M^{\\\\mathsf T} \\\\in \\\\mathbb{R}^{d \\\\times m}$, so the claimed gradient vector is $a + M^{\\\\mathsf T} c$.\n\nEverything in the statement is pointwise: $f$ and $h$ are not required to be continuous, differentiable, or bounded anywhere except as stated at the points $w_0$, $h(w_0)$, and $(w_0, h(w_0))$, and the conclusion likewise concerns only the single point $w_0$. Degenerate dimensions are included in the quantifiers: if $m = 0$, then $E_m$ is the one-point zero space, $c$ and $h(w_0)$ are necessarily its unique element $0$, $h'$ is the unique (zero) map and h'^\\\\dagger c = 0, $h$ is constant, and the conclusion coincides verbatim with hypothesis $(\\\\mathrm{ha})$; if $d = 0$ the parameter space $E_d$ is a single point and the gradient assertion becomes trivial in content. The hypotheses are jointly satisfiable \u2014 for example $f(w, v) = \\\\langle p, w\\\\rangle + \\\\langle q, v\\\\rangle$ with an affine $h$ and any $w_0$ satisfies all four, with $a = p$, $c = q$, and $h'$ the linear part \u2014 so the statement is not vacuous."\n}", "startLine": 1, "lineNumbers": [1, 2, 3]}, "meta": {"source": {"type": "internal", "value": "agent://RB-M03"}}}}