Calculus - Descent Direction
2026-09-06 · 随笔 · 43a908c205b5
优化里一句常见的话:“Newton 方向 −H−1g-H^{-1}g 是下降方向,因为 g⊤d<0g^{\top}d<0”。这句话压缩了多元微积分里的三个概念(方向导数、一阶 Taylor、链式法则)和线性代数里的一个概念(正定)。这篇把它拆开,每一步给出课本说法和 Mathlib 里对应的定义或定理。
记号:f:Rn→Rf:\mathbb R^n\to\mathbb R,当前点 θ\theta,方向 dd,梯度 g=∇f(θ)g=\nabla f(\theta),Hessian HH。
什么是下降方向
在点 θ\theta 处,方向 dd 叫下降方向,意思是沿它走一小步函数值变小:
∃ϵ>0, ∀0<t<ϵ:f(θ+td)<f(θ)\exists\,\epsilon>0,\ \forall\,0<t<\epsilon:\quad f(\theta+td)<f(\theta)
判据是 g⊤d<0g^{\top}d<0。为什么这个内积能决定下降,要靠一阶 Taylor 展开。
一阶 Taylor 展开
f(θ+td)=f(θ)+tg⊤d+o(t)f(\theta+td)=f(\theta)+t\,g^{\top}d+o(t)
tt 很小时 o(t)o(t) 可忽略,函数值的变化约等于 tg⊤dt\,g^{\top}d。t>0t>0,所以符号由 g⊤dg^{\top}d 决定:
- g⊤d<0g^{\top}d<0:下降
- g⊤d>0g^{\top}d>0:上升
- g⊤d=0g^{\top}d=0:一阶看不出,要看二阶
几何上 g⊤d=∥g∥∥d∥cos∠(g,d)g^{\top}d=\|g\|\,\|d\|\cos\angle(g,d)。梯度指向最陡上升,与它成钝角的方向都往下走。最简单的例子 d=−gd=-g,g⊤d=−∥g∥2<0g^{\top}d=-\|g\|^{2}<0,这就是梯度下降。
gg 从哪来
gg 不是新东西,就是 ∇f(θ)\nabla f(\theta) 的缩写。它出现在展开式里是链式法则的结果。
把多元函数压成一元。固定 θ\theta 和 dd,定义
φ(t)=f(θ+td)\varphi(t)=f(\theta+td)
φ\varphi 只有一个变量 tt,对它做一元 Taylor 展开:
φ(t)=φ(0)+φ′(0)⋅t+o(t)\varphi(t)=\varphi(0)+\varphi'(0)\cdot t+o(t)
φ(0)=f(θ)\varphi(0)=f(\theta)。φ′(0)\varphi'(0) 要用链式法则算,因为 φ\varphi 是复合函数:外层 ff 是多元的,内层是路径 t↦θ+tdt\mapsto\theta+td。
为什么一元函数求导会冒出 ∂\partial 和 ∑\sum
一元链式法则:h(t)=f(u(t))h(t)=f(u(t)),则 h′(t)=f′(u(t))⋅u′(t)h'(t)=f'(u(t))\cdot u'(t)。
多元时 ff 有 nn 个输入 u1,…,unu_1,\dots,u_n,每个都随 tt 变。tt 变一点,ff 的变化来自 nn 条路径,每条贡献“ff 对该输入的偏导 ×\times 该输入对 tt 的导数“,全部加起来:
dtdf(u1(t),…,un(t))=i=1∑n∂ui∂f⋅dtdui\frac{d}{dt}f\big(u_1(t),\dots,u_n(t)\big)=\sum_{i=1}^{n}\frac{\partial f}{\partial u_i}\cdot\frac{du_i}{dt}
∂\partial 出现是因为 ff 是多元的,只能求偏导;∑\sum 出现是因为 nn 个输入各贡献一份。φ′\varphi' 最终是一个数,一元函数的导数,只是算它的过程经过了多元的 ff。
代入 ui(t)=θi+tdiu_i(t)=\theta_i+td_i,有 dtdui=di\dfrac{du_i}{dt}=d_i:
φ′(0)=i∑∂θi∂f(θ)di=∇f(θ)⊤d=g⊤d\varphi'(0)=\sum_{i}\frac{\partial f}{\partial\theta_i}(\theta)\,d_i=\nabla f(\theta)^{\top}d=g^{\top}d
代回一元 Taylor 就得到开头的展开式。g⊤dg^{\top}d 也叫 ff 在 θ\theta 沿 dd 的方向导数,记 Ddf(θ)D_d f(\theta)。
例子
f(x,y)=x2+3yf(x,y)=x^{2}+3y,θ=(1,2)\theta=(1,2),d=(1,−1)d=(1,-1)。
直接算:φ(t)=f(1+t,2−t)=(1+t)2+3(2−t)=t2−t+7\varphi(t)=f(1+t,\,2-t)=(1+t)^{2}+3(2-t)=t^{2}-t+7,所以 φ′(0)=−1\varphi'(0)=-1。
用链式法则:∂x∂f=2x=2\dfrac{\partial f}{\partial x}=2x=2,∂y∂f=3\dfrac{\partial f}{\partial y}=3,于是 φ′(0)=2⋅1+3⋅(−1)=−1\varphi'(0)=2\cdot1+3\cdot(-1)=-1。
两边一致。第二种写法就是 g⊤dg^{\top}d,g=(2,3)g=(2,3),d=(1,−1)d=(1,-1)。这个方向是下降方向。
为什么 −H−1g-H^{-1}g 是下降方向
代入判据:
g⊤d=g⊤(−H−1g)=−g⊤H−1gg^{\top}d=g^{\top}\big(-H^{-1}g\big)=-\,g^{\top}H^{-1}g
关键一步:若 HH 正定,则 H−1H^{-1} 也正定(特征值全是 HH 特征值的倒数,仍为正)。正定的定义是对任意非零向量 vv 有 v⊤H−1v>0v^{\top}H^{-1}v>0。取 v=g=0v=g\ne0:
g⊤H−1g>0⇒g⊤d=−g⊤H−1g<0g^{\top}H^{-1}g>0\;\Rightarrow\;g^{\top}d=-\,g^{\top}H^{-1}g<0
所以 Newton 方向是下降方向。条件 g=0g\ne0 是在排除正定定义不覆盖的 v=0v=0;g=0g=0 时已在驻点,没有方向可谈。
隐含前提:结论依赖 HH 正定。HH 不定时(鞍点附近常见),g⊤H−1gg^{\top}H^{-1}g 可能为负,Newton 方向反而上升。这是实践里要做 damping、加 λI\lambda I 或用 trust region 的原因。
微积分还是分析
上面的推导全部属于多元微积分:链式法则怎么用、φ′(0)=g⊤d\varphi'(0)=g^{\top}d 怎么算。分析学处理的是同一批公式的“为什么成立”:
| 问题 |
归属 |
| 链式法则怎么用、φ′(0)=g⊤d\varphi'(0)=g^{\top}d 怎么算 |
微积分 |
| o(t)o(t) 到底是什么、余项怎么估计 |
分析 |
| 链式法则成立需要 ff 满足什么(可微 vs 偏导存在) |
分析 |
| 偏导都存在但函数不可微的反例 |
分析 |
| 梯度作为“使一阶近似成立的唯一线性映射”的定义 |
分析(Fréchet 导数) |
Mathlib 不分微积分和分析,全部按分析的标准写。所以下面的对应表里会多出可微性假设,那是分析层被显式化了,和 Finset.sum_comm 在矩阵证明里被显式化是同一回事。
Mathlib 对应
所有名字对照 mathlib4 master 源码(2026-09-06)。
| 步骤 |
课本说法 |
Mathlib |
| 0 |
ff 在 θ\theta 可微 |
HasFDerivAt f f' θ,f' 是 Fréchet 导数 Df(θ)Df(\theta),一个连续线性映射。不用 LL 记导数,免得和损失 L\mathcal L 混 |
| 1 |
一阶 Taylor:f(θ+h)=f(θ)+Df(θ)[h]+o(h)f(\theta+h)=f(\theta)+Df(\theta)[h]+o(h) |
hasFDerivAt_iff_isLittleO_nhds_zero。这是 HasFDerivAt 的定义,不是定理 |
| 2 |
定义 φ(t)=f(θ+td)\varphi(t)=f(\theta+td) |
HasLineDerivAt 𝕜 f f' θ d := HasDerivAt (fun t ↦ f (θ + t • d)) f' 0 |
| 3 |
路径 t↦θ+tdt\mapsto\theta+td 的导数是 dd |
hasDerivAt_id 得 11;HasDerivAt.smul_const 得 1⋅d1\cdot d;HasDerivAt.const_add 加常数不改导数 |
| 4 |
链式法则:φ′(0)=Df(θ)[d]\varphi'(0)=Df(\theta)[d] |
HasFDerivAt.comp_hasDerivAt。打包版 HasFDerivAt.hasLineDerivAt |
| 5 |
Df(θ)[d]=g⊤dDf(\theta)[d]=g^{\top}d |
gradient := (toDual 𝕜 F).symm (fderiv 𝕜 f x),Riesz 表示把泛函 Df(θ)Df(\theta) 变成向量 gg;inner_gradient_left : ⟪∇ f x, y⟫ = fderiv 𝕜 f x y |
| 6 |
g⊤d<0g^{\top}d<0 即 φ′(0)<0\varphi'(0)<0 |
代入,纯改写 |
| 7 |
导数为负 ⇒\Rightarrow 小步下降 |
HasDerivAt.tendsto_slope_zero_right:右斜率 →φ′(0)\to\varphi'(0);Filter.Tendsto.eventually_lt_const:极限为负则最终为负;t>0t>0 故 φ(t)<φ(0)\varphi(t)<\varphi(0) |
| 8 |
HH 正定 ⇒H−1\Rightarrow H^{-1} 正定 |
Matrix.PosDef.inv,双向 Matrix.posDef_inv_iff |
| 9 |
g=0⇒g⊤H−1g>0g\ne0\Rightarrow g^{\top}H^{-1}g>0 |
Matrix.PosDef.dotProduct_mulVec_pos : 0 < star x ⬝ᵥ (M *ᵥ x),取 M=H−1M=H^{-1},x=gx=g |
| 10 |
合并得 g⊤(−H−1g)<0g^{\top}(-H^{-1}g)<0 |
序公理,接第 6 步 |
值得注意的对应
- Taylor 展开在 Mathlib 里不是被证明的,是被定义的。
HasFDerivAt f f' x 的定义就是“f(x+h)−f(x)−f′(x)[h]f(x+h)-f(x)-f'(x)[h] 是 o(h)o(h)“。课本先讲导数再证 Taylor,Mathlib 反过来。”gg 怎么突然出现“在 Mathlib 里的答案是:Df(θ)Df(\theta) 从可微假设来,gg 是它经 Riesz 表示变出来的向量。
- 链式法则里的 ∂\partial 和 ∑\sum 在 Mathlib 里消失了。
comp_hasDerivAt 的结论是 HasDerivAt (l ∘ f) (l' f') x,只有“外层线性映射作用在内层导数上”这一个抽象操作。∑i∂θi∂fdi\sum_i\frac{\partial f}{\partial\theta_i}d_i 是 Df(θ)[d]Df(\theta)[d] 在标准基下的坐标展开,Mathlib 很少展开到那一层。
- “下降方向”在 Mathlib 里没有专名。 第 7 步由两个通用引理拼出:导数是右斜率的极限,极限为负则最终为负。
PosDef 的定义带 star。 IsHermitian ∧ ∀ x ≠ 0, 0 < ∑∑ star xᵢ Mᵢⱼ xⱼ,为了同时覆盖复数。实数上 star 是恒等,dotProduct_mulVec_pos 就是 x⊤Mx>0x^{\top}Mx>0。
分层
| 层 |
步骤 |
位置 |
| 微积分 |
1–7 |
Analysis/Calculus/ 下的 FDeriv、Deriv、LineDeriv、Gradient |
| 线性代数 |
8–9 |
LinearAlgebra/Matrix/PosDef.lean |
| 底层 |
7 后半、10 |
Topology/Order/ 的 filter 引理、序公理 |
一句“Newton 方向是下降方向”横跨三层,每层的工具只做一件小事。
排版备注
LaTeX 里的 \, 是细空格,φ′(0)t\varphi'(0)\,t 读作 φ′(0)⋅t\varphi'(0)\cdot t。从渲染页面复制公式时反斜杠常被吃掉,剩下一个像逗号的字符,那不是数学记号。