5.9 幂塔与不动点 · 从直觉到证明

一步一步建立直观

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

01先写出递推，而非直接画无穷高

把有限幂塔看作迭代 $x_{k+1}=b^{x_k}$ 。右图的蜘蛛网先竖直到达函数曲线，再横着回到对角线，把输出作为下一次输入。若序列真的收敛且指数函数连续，极限必满足 $x=b^x$ ；这一步给出必要条件，还没有保证收敛。

02交替接近也可能收敛

当底数小于一时，指数函数递减，迭代可能在不动点两侧往返。检查附近导数的绝对值是否小于一，有助于理解小误差是被缩小还是放大。图中几次迭代看似稳定只是线索；局部收缩还需结合进入该邻域的条件。

03不动点方程不能替代收敛证明

将底数提高后，轨迹越走越大，最终可能超出显示范围。程序会明确报告溢出范围，而不会把屏幕边缘当成极限。无穷表达式若没有先定义为一个收敛过程，就不能随意把“顶端的无穷幂塔”替换为自身并当作求值完成。

5.9.1 先说明无限符号代表哪个过程¶

写下无限幂塔之前，先定义有限迭代 $x_0=1,x_{n+1}=a^{x_n}$ 。无限表达式若要有意义，应是这个序列的极限，而不是允许任意剪掉顶部、移动括号的代数对象。

如果序列确实收敛到 $L$ ，连续性允许把极限送入函数，得到 $L=a^L$ 。这只是极限必须满足的条件，还没有保证序列收敛，也没保证方程的每个根都能从当前初值到达。

5.9.2 不动点还要分稳定与不稳定¶

取 $a=\sqrt2$ ，二与四都满足不动点方程。附近的微小偏差经过一轮迭代，大约乘以 $f'(L)=L\ln a$ 。在二处倍率小于一，偏差局部缩小；在四处倍率大于一，偏差局部放大。

把图 $y=a^x$ 与 $y=x$ 画在同一坐标系，从当前值竖直走到函数曲线，再水平走回对角线，可以追踪迭代。这样的蛛网图帮助观察靠近、远离或振荡，但严格证明仍需单调、有界或压缩等条件。

一个重要解题习惯在这里非常清楚：从“假设存在极限”推出方程之后，必须回头检查存在性。否则会把必要条件误当充分条件。Lean 定理也明确把收敛写成假设，保留了这道不能被符号操作跳过的门槛。

定义 5.9.1　幂塔的有限迭代

给定底数 $b>0$ 和起点 $x_0$ ，定义 $x_{k+1}=b^{x_k}$ 。所谓无限幂塔的取值，需要先说明这个序列的极限是否存在。

命题 5.9.1　收敛的迭代必到达不动点

若 $x_k$ 收敛到有限实数 $L$ ，则 $L=b^L$ 。该方程只是收敛的必要条件。

证明 · 展开纸笔推导

收敛序列平移一项仍趋于 $L$ ，所以 $x_{k+1}\to L$ 。函数 $x\mapsto b^x$ 在实数上连续，故 $b^{x_k}\to b^L$ 。

迭代两边逐项相等，极限的唯一性给出 $L=b^L$ 。证明从“序列收敛”开始，不能倒过来用同一个推理宣称只要方程有解，所有初值的迭代就会收敛。

□

数学表述 5.9.1¶

无限幂塔应先定义为有限迭代，再讨论其极限。如果迭代确实收敛，极限才必须满足不动点方程。

对 $a>0$ ，令 $x_0=1,x_{n+1}=a^{x_n}$ 。若 $x_n\to L$ ，由连续性得到 $L=a^L$ 。局部稳定性的常用线性判据是 $|a^L\ln a|=|L\ln a|<1$ 。

例 5.9.1 把概念用于具体计算

$a=\sqrt2$ 时 $L=2$ 和 $L=4$ 都满足方程；在前者的导数为 $\ln2<1$ ，后者为 $2\ln2>1$ 。不动点不一定是从给定初值可达的稳定极限。

练习 5.9.1¶

$a=1$ 时该迭代的每一项与极限？

展开解答与检查

都为 $1$ 。

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

完整证明一般连续迭代在已知收敛时，其极限为不动点；收敛是假设，绝不隐含在代数方程里。

Lockdown.tower_limit_fixed_point

theorem tower_limit_fixed_point (f : ℝ → ℝ) (u : ℕ → ℝ) (L : ℝ)
    (hc : ContinuousAt f L) (hu : Filter.Tendsto u Filter.atTop (nhds L))
    (hs : ∀ n, u (n+1)=f (u n)) : f L=L := by
  have hshift : Filter.Tendsto (fun n => u (n+1)) Filter.atTop (nhds L) :=
    hu.comp (Filter.tendsto_add_atTop_nat 1)
  have hfun : (fun n => f (u n)) = fun n => u (n+1) := by
    funext n
    exact (hs n).symm
  have hf := hc.tendsto.comp hu
  change Filter.Tendsto (fun n => f (u n)) _ _ at hf
  rw [hfun] at hf
  exact tendsto_nhds_unique hf hshift

查看完整定义与上下文 ↗ · 全书证明范围

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

先定义有限迭代，再检查收敛；区分不动点方程与稳定性。

官方课程与图示 ↗ · 原视频 ↗

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