5.6 虚数利率与连续旋转 · 从直觉到证明

一步一步建立直观

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

实数复利每一步乘以 $1+r\Delta t$ 。若把增长率换成 $i$ ，一步变成乘以 $1+i\Delta t$ ，它近似一次小旋转，却还带着略大于一的模长。右图显示连续极限的圆周轨迹，而不是直接播放有限次复利步骤。

单步模长为 $\sqrt{1+\Delta t^2}$ ，偏离一的主要量是二阶；完成固定总时间需要的一阶数量级步数，不足以留下非零的二阶累计模长误差。另一方面，每步的一阶转角会积成有限总角度。这是旋转留下、额外膨胀消失的原因。

螺线情形故意加入非零实部，表示方程中真实存在的径向增长。它不会因为时间步细分而消失；有限步虚数复利的模长偏差则会在极限中消失。两幅外观相似的螺线可能来自不同机制，必须根据更新规则区分。

普通复利每步按当前量增加一小部分。若把增量乘上 $\mathrm i$ ，新增部分不再沿原方向，而是垂直于原方向。一步变成乘 $1+\mathrm i h$ ，不断重复，就得到一条绕原点前进的折线轨迹。

每步到底是不是旋转？它的模长为 $\sqrt{1+h^2}>1$ ，所以还夹带一点向外扩张。图像若只强调绕圈，容易隐藏这个有限步误差。精确的圆周运动来自步长趋零后的极限，而不是任意有限步都在圆上。

固定总时间 $t$ ，分成 $n$ 步，模长倍率是 $(1+t^2/n^2)^{n/2}$ 。单步误差是二阶的，总步数只是一阶增加；取对数后约为 $t^2/(2n)$ ，趋向零，所以总模长趋向一。

角度每步增加 $\arctan(t/n)$ ，总角度为 $n\arctan(t/n)$ ，趋向 $t$ 。模长和角度两个条件合起来，解释了极限为何是 $\mathrm e^{\mathrm it}$ 。这里用到的局部近似必须在小步长下理解。

这个例子也说明欧拉数值法可能产生什么误差：真实系统守恒半径，有限切向步却慢慢漂离。把步数加倍，观察偏差变化，会比单看一条漂亮轨迹更有教学价值。Lean 只核验单步模长恒等式，收敛论证仍需另外完成。

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

把复利每一步的增长率改成纯虚数，每个小步就增加一个切向位移；步长越来越小时，轨迹趋于圆周运动。

离散近似为 $(1+\mathrm{i} t/n)^n$ 。单步模长平方为 $1+(t/n)^2$ ，整个模长为 $(1+t^2/n^2)^{n/2}$ ，其极限为 $1$ 。

例 5.6.1 把概念用于具体计算

单步取 $h=0.1$ ， $1+0.1\mathrm{i}$ 的模长是 $\sqrt{1.01}>1$ ；有限步的轨迹略向外扩张，这个误差在连续极限消失。

$h=1$ 时，乘 $1+\mathrm{i}$ 后角度和模长怎样变化？

展开解答与检查

增加 $\pi/4$ ，模长乘 $\sqrt2$ 。

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

验证单步复数的模长平方公式。复利序列收敛到复指数的极限定理未在此命题中形式化。

Lockdown.imaginary_step_norm

theorem imaginary_step_norm (h : ℝ) :
    Complex.normSq (1+(h:ℂ)*Complex.I)=1+h^2 := by
  simp [Complex.normSq_apply, pow_two]

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

仔细区分有限切向步与精确圆周运动，追踪有限步的模长误差。

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