4.8 动态理解欧拉恒等式 · 从直觉到证明

一步一步建立直观

先预测，再点“演示本步”核对右图。每一步都重设到指定情形，随后可以自由修改参数。

余弦和正弦组成的位置 $(\cos t,\sin t)$ 从 $(1,0)$ 出发，速度是位置旋转直角后的向量。复指数 $e^{it}$ 满足同样的局部规则与初值。若调用相应微分方程的唯一性，两种表达就描述同一运动，而不只是偶然在几个角度上数值相同。

当时间走到半圈，横坐标为负一、纵坐标为零，因此 $e^{i\pi}=-1$ 。右图保留速度箭头，强调等式中的常数来自整条连续运动在特殊时刻的位置。它不是把五个符号强行拼在一起，而是指数结构与圆周几何的交汇。

把实部增长率调正，点仍旋转，但半径不再固定。此时半圈位置不再是负一，而是负实轴上一个更远的点。这个对照帮助检验欧拉公式的准确条件：纯虚指数只改变相位，加入实部还会乘上实指数的模长因子。

从复平面的点一出发，让速度永远等于当前位置乘以 $\mathrm i$ 。速度与半径垂直，长度与半径相同，所以它沿单位圆以单位角速度运动。走过时间 $t$ 后的位置应是 $\cos t+\mathrm i\sin t$ 。

另一边，指数函数 $\mathrm e^{\mathrm it}$ 对时间的导数是 $\mathrm i\mathrm e^{\mathrm it}$ ，起点也是一。两个表达式满足同一微分方程和初值，在相应唯一性结论下，它们就是同一条轨迹。欧拉公式因此可被理解为两种描述相遇。

时间 $\pi/2$ 到达 $\mathrm i$ ，时间 $\pi$ 到达负一，时间 $2\pi$ 回到一。著名恒等式是半圈位置的记录；若只背五个常数排在一起，就会丢失背后的完整连续运动。

在动画中暂停于四分之一圈和半圈，分别读横纵分量，再把它们与余弦正弦对应。改变转动方向只改变到达路径，走正半圈或负半圈都到负一，这也展示了指数的周期性。

周期性将在复对数中变成多值性：同一个终点可以对应许多角度，所以从终点反推指数不能保持全局唯一。欧拉公式既统一了指数与三角，也提醒我们把实数反函数的习惯推广到复数时需要重新检查。

与本图相连的定义与证明：5.4 · 乘以 i 保持长度并旋转直角。本节的具体条件与形式化范围见下文。

复指数 $\mathrm{e}^{\mathrm{i} t}$ 从 $1$ 出发沿单位圆运动，走过 $\pi$ 弧度后到达 $-1$ 。

$\mathrm{e}^{\mathrm{i} t}=\cos t+\mathrm{i}\sin t$ ，所以 $\mathrm{e}^{\mathrm{i}\pi}+1=0$ 。也可比较两边的微分方程 $z'=\mathrm{i} z$ 与初始值 $z(0)=1$ ，在唯一性定理下识别二者。

例 4.8.1 把概念用于具体计算

$t=\pi/2$ 时值为 $\mathrm{i}$ ， $t=2\pi$ 时回到 $1$ 。四个四分之一圈的乘积为 $\mathrm{i}^4=1$ 。

$\mathrm{e}^{-\mathrm{i}\pi}$ 是多少？

展开解答与检查

同样为 $-1$ ；方向不同，终点相同。

Lean 对照 4.8.1 命题、证明与适用边界

完整验证复指数的欧拉恒等式，复用 mathlib 已证明的结论。

DifferentialEquations.euler_identity

theorem euler_identity : Complex.exp ((Real.pi:ℂ)*Complex.I) = -1 := by
  exact Complex.exp_pi_mul_I

原课对照观课问题、视频与图示

暂停在四分之一圈和半圈，读取复平面坐标并解释欧拉恒等式。

点击后连接 YouTube；播放器不可用时可通过上方原链接观看。