一般性的概念
2026-09-06 · 随笔 · 43a908c205b5
一个词可能有很多的歧义
比如我们之前看到的gpio
可能指的是1. 电路 2. 接口 3. ?
我们以梯度为例尝试解释:
梯度是 (类型: 向量?)
xx的梯度?
xxx的梯度? 可能有很多梯度吗
它表示(xx语义)
形式是:
mathlib里面 如何定义:
实际应用中:
gg 不是新东西,就是 ∇f(θ)\nabla f(\theta) 的缩写,前面定义过 gt:=∇ft(θt)g_t:=\nabla f_t(\theta_t)。它出现在展开式里是链式法则的结果。
从一元 Taylor 推过来
把多元函数压成一元:固定 θ\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),t+o(t)
φ(0)=f(θ)\varphi(0)=f(\theta) 显然。φ′(0)\varphi'(0) 用链式法则算:θ+td\theta+td 的第 ii 个分量是 θi+tdi\theta_i+td_i,对 tt 求导得 did_i,所以
φ′(t)=i∑∂θi∂f(θ+td)⋅di
\varphi'(t)=\sum_i \frac{\partial f}{\partial\theta_i}(\theta+td)\cdot d_i
在 t=0t=0:
φ′(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
把这两个代回去就得到
f(θ+td)=f(θ)+t,g⊤d+o(t)
f(\theta+td)=f(\theta)+t,g^{\top}d+o(t)
直觉
一元里 f(x+h)≈f(x)+f′(x)hf(x+h)\approx f(x)+f'(x)h,斜率乘位移。多元里位移是向量 tdtd,“斜率”是梯度向量 gg,两者相乘只能用内积,于是 f′(x)hf'(x)h 变成 g⊤(td)=t,g⊤dg^{\top}(td)=t,g^{\top}d。梯度的定义本身就是“使这个一阶近似成立的那个向量”。
为什么是 g⊤dg^{\top}d 而不是别的组合
内积 g⊤d=∑igidig^{\top}d=\sum_i g_i d_i 的含义是:沿 dd 走,每个坐标 θi\theta_i 变了 did_i,函数因此变了约 gidig_i d_i,把各坐标的贡献加起来。方向导数就是这个东西,记作 Ddf(θ)=g⊤dD_d f(\theta)=g^{\top}d。
迹只要对角线元素,也就是 j=ij=i。把定义里的 jj 换成 ii:
(AB)ii=∑k=1nAikBki
(AB){ii}=\sum{k=1}^{n}A_{ik}B_{ki}
AA 的第 ii 行点乘 BB 的第 ii 列。这就是你问的那一步,没有别的操作。
再套上外层求和
tr(AB)=i=1∑m(AB)ii=∑i=1mk=1∑nAikBki
\operatorname{tr}(AB)=\sum_{i=1}^{m}(AB){ii}=\sum{i=1}^{m}\sum_{k=1}^{n}A_{ik}B_{ki}
2×22\times2 具体算一遍
A=(a11a12\a21a22),B=(b11b12\b21b22)
A=\begin{pmatrix}a_{11}&a_{12}\a_{21}&a_{22}\end{pmatrix},\qquad
B=\begin{pmatrix}b_{11}&b_{12}\b_{21}&b_{22}\end{pmatrix}
AB=(a11b11+a12b21a11b12+a12b22 a21b11+a22b21a21b12+a22b22)
AB=\begin{pmatrix}
a_{11}b_{11}+a_{12}b_{21} & a_{11}b_{12}+a_{12}b_{22}\
a_{21}b_{11}+a_{22}b_{21} & a_{21}b_{12}+a_{22}b_{22}
\end{pmatrix}
左上角 (AB)11=a11b11+a12b21=∑ka1kbk1(AB){11}=a{11}b_{11}+a_{12}b_{21}=\sum_k a_{1k}b_{k1},第一行点第一列。
右下角 (AB)22=a21b12+a22b22=∑ka2kbk2(AB){22}=a{21}b_{12}+a_{22}b_{22}=\sum_k a_{2k}b_{k2},第二行点第二列。
tr(AB)=a11b11+a12b21+a21b12+a22b22
\operatorname{tr}(AB)=a_{11}b_{11}+a_{12}b_{21}+a_{21}b_{12}+a_{22}b_{22}
(AB)ij=∑k=1nAikBkj
(AB){ij}=\sum{k=1}^{n}A_{ik}B_{kj}
含义:AA 的第 ii 行与 BB 的第 jj 列做点积。kk 跑遍 AA 的列数 = BB 的行数,也就是“中间那个维度”。
取对角线
迹只要对角线元素,也就是 j=ij=i。把定义里的 jj 换成 ii:
(AB)ii=∑k=1nAikBki
(AB){ii}=\sum{k=1}^{n}A_{ik}B_{ki}
AA 的第 ii 行点乘 BB 的第 ii 列。这就是你问的那一步,没有别的操作。
再套上外层求和
tr(AB)=i=1∑m(AB)ii=∑i=1mk=1∑nAikBki
\operatorname{tr}(AB)=\sum_{i=1}^{m}(AB){ii}=\sum{i=1}^{m}\sum_{k=1}^{n}A_{ik}B_{ki}
2×22\times2 具体算一遍
A=(a11a12\a21a22),B=(b11b12\b21b22)
A=\begin{pmatrix}a_{11}&a_{12}\a_{21}&a_{22}\end{pmatrix},\qquad
B=\begin{pmatrix}b_{11}&b_{12}\b_{21}&b_{22}\end{pmatrix}
AB=(a11b11+a12b21a11b12+a12b22 a21b11+a22b21a21b12+a22b22)
AB=\begin{pmatrix}
a_{11}b_{11}+a_{12}b_{21} & a_{11}b_{12}+a_{12}b_{22}\
a_{21}b_{11}+a_{22}b_{21} & a_{21}b_{12}+a_{22}b_{22}
\end{pmatrix}
左上角 (AB)11=a11b11+a12b21=∑ka1kbk1(AB){11}=a{11}b_{11}+a_{12}b_{21}=\sum_k a_{1k}b_{k1},第一行点第一列。
右下角 (AB)22=a21b12+a22b22=∑ka2kbk2(AB){22}=a{21}b_{12}+a_{22}b_{22}=\sum_k a_{2k}b_{k2},第二行点第二列。
tr(AB)=a11b11+a12b21+a21b12+a22b22
\operatorname{tr}(AB)=a_{11}b_{11}+a_{12}b_{21}+a_{21}b_{12}+a_{22}b_{22}
四项,每项下标形状都是 aikbkia_{ik}b_{ki},ii 和 kk 各取 1,21,2。
在 Mathlib 里
这一步就是 Matrix.mul_apply:
lean
theorem Matrix.mul_apply : (M * N) i k = ∑ j, M i j * N j k
对迹的推导里用它时 i = k,Lean 会自动把两个下标统一。所以 trace_transpose_mul 那个证明只写了 Finset.sum_comm,是因为 trace 和 * 的定义展开(mul_apply)是定义性相等,rfl 级别,不需要显式引用。