一行公式
f(θ+td)=f(θ)+tg⊤d+o(t),g=∇f(θ)f(\theta+td)=f(\theta)+t\,g^{\top}d+o(t),\qquad g=\nabla f(\theta)
θ\theta 是当前点,dd 是方向,t>0t>0 是步长。g⊤dg^{\top}d 是 ff 在 θ\theta 沿 dd 的方向导数。o(t)o(t) 是余项的缩写。严格说:令 r(t)=f(θ+td)−f(θ)−tg⊤dr(t)=f(\theta+td)-f(\theta)-t\,g^{\top}d,则断言 limt→0r(t)/t=0\lim_{t\to0}r(t)/t=0。
导数在哪:上面那行把导数藏进了 gg。写全是一条链。先是可微的定义,导数 Df(θ)Df(\theta) 作用在位移 tdtd 上:
f(θ+td)=f(θ)+Df(θ)[td]+o(t)f(\theta+td)=f(\theta)+Df(\theta)[td]+o(t)
然后把 Df(θ)[td]Df(\theta)[td] 一步步改写成 tg⊤dt\,g^{\top}d:
Df(θ)[td]=线性tDf(θ)[d]=Rieszt⟨g,d⟩=记法tg⊤dDf(\theta)[td]\;\overset{\text{线性}}{=}\;t\,Df(\theta)[d]\;\overset{\text{Riesz}}{=}\;t\,\langle g,d\rangle\;\overset{\text{记法}}{=}\;t\,g^{\top}d
第一行是近似(余项 o(t)o(t)),第二行三个等号都是恒等式。导数一律写 Df(θ)Df(\theta),Lean 片段里按 Mathlib 习惯叫 f';字母 L\mathcal L 只用于损失函数,不用来表示导数。
先给每个记号一个类型(Mathlib 写法,Rn\mathbb R^n 记 EuclideanSpace ℝ (Fin n),它是带 2-范数的 Fin n → ℝ):
| 记号 |
类型 |
说明 |
| θ\theta, dd |
EuclideanSpace ℝ (Fin n) |
点和方向是同一种东西,都是 Rn\mathbb R^n 里的向量 |
| tt |
ℝ |
标量 |
| θ+td\theta+td |
EuclideanSpace ℝ (Fin n) |
Lean 写 θ + t • d,• 是标量乘向量 |
| ff |
EuclideanSpace ℝ (Fin n) → ℝ |
输入向量,输出一个数 |
| φ\varphi |
ℝ → ℝ |
fun t => f (θ + t • d),一元函数 |
| φ′(0)\varphi'(0) |
ℝ |
一元导数,撇号记法:φ′(0)=limt→0tφ(t)−φ(0)\varphi'(0)=\lim_{t\to0}\frac{\varphi(t)-\varphi(0)}{t}。deriv φ 0,命题形式 HasDerivAt φ φ' 0 |
| Df(θ)Df(\theta) |
EuclideanSpace ℝ (Fin n) →L[ℝ] ℝ |
连续线性映射。fderiv ℝ f θ,Mathlib 引理里常叫 f'。输入方向,输出一阶变化量 |
| Df(θ)[d]Df(\theta)[d] |
ℝ |
导数作用在方向上,一个数 |
| g=∇f(θ)g=\nabla f(\theta) |
EuclideanSpace ℝ (Fin n) |
gradient f θ,和 θ\theta、dd 同类型 |
| g⊤dg^{\top}d |
ℝ |
inner ℝ g d,写 ⟪g, d⟫。inner_gradient_left 说它等于 fderiv ℝ f θ d |
| ∂θi∂f(θ)\dfrac{\partial f}{\partial\theta_i}(\theta) |
ℝ |
Df(θ)Df(\theta) 作用在第 ii 个基向量上:fderiv ℝ f θ (EuclideanSpace.single i 1) |
| rr |
ℝ → ℝ |
余项函数 r(t)=φ(t)−φ(0)−φ′(0)tr(t)=\varphi(t)-\varphi(0)-\varphi'(0)\,t |
| o(t)o(t) |
不是一个值,是一个命题 |
r =o[𝓝 0] (fun t => t),即 Asymptotics.IsLittleO。展开是 ∀ε>0, ∃δ>0, 0<∣t∣<δ⇒∣r(t)∣≤ε∣t∣\forall\varepsilon>0,\ \exists\delta>0,\ 0<\lvert t\rvert<\delta\Rightarrow\lvert r(t)\rvert\le\varepsilon\lvert t\rvert |
注意最后一行。课本里 o(t)o(t) 像一个数,可以加到等式右边;在 Lean 里它是关于余项函数 r(t)=φ(t)−φ(0)−φ′(0)tr(t)=\varphi(t)-\varphi(0)-\varphi'(0)t 的断言:r=o(t)r=o(t)。所以“f(θ+td)=f(θ)+tg⊤d+o(t)f(\theta+td)=f(\theta)+t\,g^{\top}d+o(t)“的严格写法是两句话:定义 rr,然后断言 r =o[𝓝 0] id。
矩阵版对应的类型:
| 记号 |
类型 |
说明 |
| WW, ΔW\Delta W, GG |
Matrix (Fin n) (Fin m) ℝ |
三个同类型,和 θ\theta、dd、gg 同类型是一个道理 |
| L\mathcal L |
Matrix (Fin n) (Fin m) ℝ → ℝ |
损失函数本身,普通函数,和 ff 同一层,不要求线性 |
| DL(W)D\mathcal L(W) |
Matrix (Fin n) (Fin m) ℝ →L[ℝ] ℝ |
导数,和 Df(θ)Df(\theta) 同一层,连续线性。fderiv ℝ 𝓛 W |
| DL(W)[H]D\mathcal L(W)[H] |
ℝ |
导数作用在更新方向 HH 上,等于 ⟨G,H⟩F\langle G,H\rangle_F |
| Tr(G⊤ΔW)\operatorname{Tr}(G^{\top}\Delta W) |
ℝ |
Matrix.trace (Gᵀ * ΔW),G⊤ΔWG^{\top}\Delta W 是 m×mm\times m 方阵 |
| ⟨G,ΔW⟩F\langle G,\Delta W\rangle_F |
ℝ |
∑ i, ∑ j, G i j * ΔW i j |
| ∣ΔW∣F|\Delta W|_F |
ℝ |
Matrix.frobenius_norm_def。Mathlib 里矩阵默认范数不是 Frobenius,要显式选这个实例 |
它从哪来:三步。
第一步,把多元函数压成一元。固定 θ\theta 和 dd,定义
φ(t)=f(θ+td),φ:R→R\varphi(t)=f(\theta+td),\qquad \varphi:\mathbb R\to\mathbb R
第二步,φ\varphi 只有一个变量,所以有普通的一元导数(撇号记法)。在 t=0t=0 处:
φ′(0)=t→0limtφ(t)−φ(0)\varphi'(0)=\lim_{t\to0}\frac{\varphi(t)-\varphi(0)}{t}
含义是从 θ\theta 出发沿 dd 刚起步时 ff 的变化率。
第三步,对一元函数 φ\varphi 做一阶 Taylor 展开,这是整段的关键一行:
φ(t)=φ(0)+φ′(0)t+o(t)\boxed{\;\varphi(t)=\varphi(0)+\varphi'(0)\,t+o(t)\;}
把 φ(t)=f(θ+td)\varphi(t)=f(\theta+td)、φ(0)=f(θ)\varphi(0)=f(\theta) 代回去,和开头那行逐项对照,就能看出 φ′(0)\varphi'(0) 应该等于什么。它怎么用链式法则算出来、为什么会出现 ∂\partial 和 ∑\sum,留给第 3、4、5 题自己推。
两步要分开:“可微给出一阶项 Df(θ)[td]Df(\theta)[td] 加余项”是近似;“把线性映射 Df(θ)Df(\theta) 写成 g⊤dg^{\top}d“是精确恒等式(Riesz 表示)。Mathlib 里前者是 HasFDerivAt 的定义,后者是 gradient 的定义。
矩阵版:参数是矩阵 WW 时,同一行公式写成 L(W+ΔW)=L(W)+Tr(G⊤ΔW)+o(∥ΔW∥F)\mathcal L(W+\Delta W)=\mathcal L(W)+\operatorname{Tr}(G^{\top}\Delta W)+o(\|\Delta W\|_F),其中 Tr(G⊤ΔW)=⟨G,ΔW⟩F=∑i,jGijΔWij\operatorname{Tr}(G^{\top}\Delta W)=\langle G,\Delta W\rangle_F=\sum_{i,j}G_{ij}\Delta W_{ij}。
相关阅读:Calculus - Descent Direction。
题目
1. o(t)o(t) 的含义
展开式里的 o(t)o(t) 是什么意思?
- 一类函数的记号:余项 r(t)r(t) 满足 limt→0r(t)/t=0\lim_{t\to0}r(t)/t=0,等价地 ∀ε>0∃δ>0\forall\varepsilon>0\,\exists\delta>0,0<∣t∣<δ⇒∣r(t)∣≤ε∣t∣0<\lvert t\rvert<\delta\Rightarrow\lvert r(t)\rvert\le\varepsilon\lvert t\rvert
- 一个绝对值小于 tt 的常数
- 二阶项 21t2d⊤Hd\tfrac12 t^{2}d^{\top}Hd 本身
- 数值计算里的舍入误差
解析
o(t)o(t) 不是一个具体的量,是一类函数的记号:所有满足 limt→0r(t)/t=0\lim_{t\to0}r(t)/t=0 的 rr。三层写法从松到紧:r(t)=o(t)r(t)=o(t);limt→0r(t)/t=0\lim_{t\to0}r(t)/t=0;∀ε>0∃δ>0∀t, 0<∣t∣<δ⇒∣r(t)∣≤ε∣t∣\forall\varepsilon>0\,\exists\delta>0\,\forall t,\ 0<\lvert t\rvert<\delta\Rightarrow\lvert r(t)\rvert\le\varepsilon\lvert t\rvert。Mathlib 取第三种当定义(isLittleO_iff),因为它不用除法,在 tt 是向量时也成立;第二种是定理 isLittleO_iff_tendsto,要求分母为 0 时分子也为 0。二阶项 21t2d⊤Hd\tfrac12t^{2}d^{\top}Hd 确实属于 o(t)o(t),但 o(t)o(t) 不等于它,余项可能还有三阶、四阶,也可能根本没有二阶展开(只要求一阶可微)。
2. 谁是自变量
定义 φ(t)=f(θ+td)\varphi(t)=f(\theta+td)。φ\varphi 的自变量是谁?
- tt
- θ\theta
- dd
- θ+td\theta+td
解析
θ\theta 和 dd 在定义 φ\varphi 时就固定了,只有 tt 在变。这就是“把多元函数压成一元”的意思:沿一条直线走,位置只由一个数 tt 决定。所以 φ′\varphi' 只能是对 tt 求导。
2b. Df(θ)Df(\theta) 的类型
Df(θ)Df(\theta),即 fderiv ℝ f θ。它的类型是?
ℝ,一个数EuclideanSpace ℝ (Fin n),一个向量EuclideanSpace ℝ (Fin n) →L[ℝ] ℝ,一个连续线性映射EuclideanSpace ℝ (Fin n) → ℝ,和 ff 同类型
解析
导数不是数也不是向量,是“输入方向、输出一阶变化量”的规则,所以是映射。它线性(→ₗ)且连续(→L)。gg 是把这个映射用内积表示出来的那个向量,Df(θ)[d]=⟨g,d⟩Df(\theta)[d]=\langle g,d\rangle,两者类型不同但信息相同(Riesz 表示)。D 错在 ff 一般不线性。
2c. o(t)o(t) 的类型
在 Lean 里,“r(t)=o(t)r(t)=o(t)” 是什么?
- 一个类型为
ℝ 的值,可以和 tg⊤dt\,g^{\top}d 相加
- 一个命题:
(fun t => r t) =o[𝓝 0] (fun t => t),断言余项函数 rr 比 tt 更快趋于 0
- 一个类型为
ℝ → ℝ 的函数,就是 rr 本身
- 一个类型为
EuclideanSpace ℝ (Fin n) 的向量
解析
课本把 o(t)o(t) 写在等式右边像一个加项,那是缩写。严格地说先定义 r(t)=φ(t)−φ(0)−φ′(0)tr(t)=\varphi(t)-\varphi(0)-\varphi'(0)\,t(这是一个 ℝ → ℝ),然后断言 r =o[𝓝 0] id。Asymptotics.IsLittleO 的值是 Prop。所以“等式里有 o(t)o(t)“其实是”等式加一条关于 rr 的断言“。这也是为什么 HasFDerivAt 的定义就是这条断言:第 9 题。
3. φ′(0)\varphi'(0) 是什么
用 g=∇f(θ)g=\nabla f(\theta) 和 dd 写出 φ′(0)\varphi'(0)。
解析
φ′(0)=i∑∂θi∂f(θ)di=g⊤d\varphi'(0)=\sum_{i}\frac{\partial f}{\partial\theta_i}(\theta)\,d_i=g^{\top}d
写成 d⊤gd^{\top}g、⟨g,d⟩\langle g,d\rangle、g⋅dg\cdot d 都是同一个数,内积对称。它有自己的名字:方向导数 Ddf(θ)D_df(\theta)。
4. 为什么一元导数里冒出 ∂\partial 和 ∑\sum
φ\varphi 是一元函数,但算 φ′(t)\varphi'(t) 时写成 ∑i∂θi∂f(θ+td)⋅di\sum_i\frac{\partial f}{\partial\theta_i}(\theta+td)\cdot d_i。∂\partial 和 ∑\sum 从哪来?
- 因为 φ\varphi 其实是多元函数
- 因为 φ\varphi 是复合函数,外层 ff 有 nn 个输入,链式法则要对每个输入求偏导再把 nn 份贡献加起来
- 因为 tt 是向量
- 这是 Taylor 展开的定义,不需要解释
解析
φ=f∘u\varphi=f\circ u,内层 u(t)=θ+tdu(t)=\theta+td 有 nn 个分量 ui(t)=θi+tdiu_i(t)=\theta_i+td_i。多元链式法则:dtdf(u1,…,un)=∑i∂ui∂fdtdui\frac{d}{dt}f(u_1,\dots,u_n)=\sum_i\frac{\partial f}{\partial u_i}\frac{du_i}{dt}。∂\partial 是因为 ff 多元,只能求偏导;∑\sum 是因为 nn 条路径各贡献一份。dtdui=di\frac{du_i}{dt}=d_i。
5. 数值题
f(x,y)=x2+3yf(x,y)=x^{2}+3y,θ=(1,2)\theta=(1,2),d=(1,−1)d=(1,-1)。
梯度 g=∇f(θ)g=\nabla f(\theta),写成 (x,y)(x,y):
φ′(0)=g⊤d\varphi'(0)=g^{\top}d 的值:
解析
∂x∂f=2x=2\frac{\partial f}{\partial x}=2x=2,∂y∂f=3\frac{\partial f}{\partial y}=3,所以 g=(2,3)g=(2,3)。g⊤d=2⋅1+3⋅(−1)=−1g^{\top}d=2\cdot1+3\cdot(-1)=-1。
验算:直接代入 φ(t)=(1+t)2+3(2−t)=t2−t+7\varphi(t)=(1+t)^{2}+3(2-t)=t^{2}-t+7,φ′(0)=−1\varphi'(0)=-1,一致。
6. 下降方向的判据
在点 θ\theta,方向 dd 是下降方向(沿它走足够小的一步函数值变小)的一阶判据是什么?
- ∥d∥<1\|d\|<1
- g⊤d>0g^{\top}d>0
- g⊤d<0g^{\top}d<0
- d=−gd=-g
解析
f(θ+td)−f(θ)=tg⊤d+o(t)f(\theta+td)-f(\theta)=t\,g^{\top}d+o(t),t>0t>0 很小时符号由 g⊤dg^{\top}d 决定。d=−gd=-g 是一个下降方向(此时 g⊤d=−∥g∥2<0g^{\top}d=-\|g\|^{2}<0),但不是唯一的:所有与 gg 成钝角的方向都下降。
7. 一阶看不出的情形
g=(2,3)g=(2,3),d=(−3,2)d=(-3,2)。沿 dd 走一小步,ff 怎么变?
- 一定下降
- 一定上升
- 不变
- 一阶判断不了,g⊤d=0g^{\top}d=0,要看二阶
解析
g⊤d=2⋅(−3)+3⋅2=0g^{\top}d=2\cdot(-3)+3\cdot2=0,dd 与梯度正交。一阶项消失,变化量是 o(t)o(t),符号由二阶项 21t2d⊤Hd\tfrac12t^{2}d^{\top}Hd 决定,而 HH 题目没给。C 是错的:o(t)o(t) 不是 0。
8. 哪一步是近似
矩阵版推导分两步:(甲)Fréchet 可微给出 L(W+ΔW)−L(W)=DL(W)[ΔW]+R(ΔW)\mathcal L(W+\Delta W)-\mathcal L(W)=D\mathcal L(W)[\Delta W]+R(\Delta W);(乙)梯度表示导数,DL(W)[H]=⟨G,H⟩F=Tr(G⊤H)D\mathcal L(W)[H]=\langle G,H\rangle_F=\operatorname{Tr}(G^{\top}H)。哪一步含近似?
- 只有甲。乙是精确恒等式
- 只有乙。甲是定义
- 两步都是近似
- 两步都是精确的
解析
甲把 R(ΔW)R(\Delta W) 丢掉才变成 ≈\approx,近似在这里,严格含义是 R=o(∥ΔW∥F)R=o(\|\Delta W\|_F)。乙只是把一个线性映射用内积写出来(Riesz 表示),再用有限求和恒等式把内积改写成迹,没有任何舍弃。这是 FirstOrderMatrixLoss 那篇文章开头强调的“两个必须分开的步骤”。
9. Mathlib 里的定义
HasFDerivAt f f' x 在 Mathlib 里等价于下面哪一条?
- ff 的所有偏导数在 xx 处存在
- h↦f(x+h)−f(x)−f′(x)[h]h\mapsto f(x+h)-f(x)-f'(x)[h] 是 o(h)o(h),当 h→0h\to0
- limh→0hf(x+h)−f(x)\lim_{h\to0}\frac{f(x+h)-f(x)}{h} 存在
- ff 在 xx 处连续
解析
hasFDerivAt_iff_isLittleO_nhds_zero 就是这条。课本先讲导数再证 Taylor,Mathlib 反过来:一阶 Taylor 展开就是可微的定义。A 太弱,偏导都存在不保证可微;C 是一元导数,多元时 hh 是向量,除不了;D 更弱。
10. 矩阵版的数值验证
G=(1201)G=\begin{pmatrix}1&0\\2&1\end{pmatrix},ΔW=(1011)\Delta W=\begin{pmatrix}1&1\\0&1\end{pmatrix}。
Frobenius 内积 ⟨G,ΔW⟩F=∑i,jGijΔWij\langle G,\Delta W\rangle_F=\sum_{i,j}G_{ij}\Delta W_{ij} 的值:
Tr(G⊤ΔW)\operatorname{Tr}(G^{\top}\Delta W) 的值:
解析
逐位相乘:1⋅1+0⋅1+2⋅0+1⋅1=21\cdot1+0\cdot1+2\cdot0+1\cdot1=2。
G⊤=(1021)G^{\top}=\begin{pmatrix}1&2\\0&1\end{pmatrix},G⊤ΔW=(1031)G^{\top}\Delta W=\begin{pmatrix}1&3\\0&1\end{pmatrix},迹 =1+1=2=1+1=2。
两者相等不是巧合:Tr(G⊤H)=∑j∑iGijHij\operatorname{Tr}(G^{\top}H)=\sum_j\sum_i G_{ij}H_{ij},换一下求和顺序就是 Frobenius 内积。Tr(ΔWG⊤)\operatorname{Tr}(\Delta W\,G^{\top}) 也等于 2,那是 trace_mul_comm。
11. 哪一步用了 Finset.sum_comm
推导 Tr(G⊤H)=⟨G,H⟩F\operatorname{Tr}(G^{\top}H)=\langle G,H\rangle_F:
Tr(G⊤H)=(a)j∑(G⊤H)jj=(b)j∑i∑(G⊤)jiHij=(c)j∑i∑GijHij=(d)i∑j∑GijHij\operatorname{Tr}(G^{\top}H)
\overset{(a)}{=}\sum_{j}(G^{\top}H)_{jj}
\overset{(b)}{=}\sum_{j}\sum_{i}(G^{\top})_{ji}H_{ij}
\overset{(c)}{=}\sum_{j}\sum_{i}G_{ij}H_{ij}
\overset{(d)}{=}\sum_{i}\sum_{j}G_{ij}H_{ij}
哪一步是 Finset.sum_comm?
解析
(a) 是迹的定义 Matrix.trace;(b) 是矩阵乘法定义 Matrix.mul_apply;(c) 是转置定义 Matrix.transpose_apply;(d) 交换两个求和号,才是 Finset.sum_comm。这条链和 Trace 篇里 trace_transpose_mul 的证明是同一批工具。