5.10 为什么 i 的 i 次方可以是实数

一步一步建立直观

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

01先为复数选择一个角度

单位虚数 $i$ 位于单位圆的上端，主辐角为 $\pi/2$ ，但加上任意整数圈仍表示同一个点。右图位置只能显示点本身，不能区分绕了多少圈。复对数必须记录所选辐角，因此同一个非零复数会对应不同的对数值。

02把指数定义中的分支写出来

若取主值， $\log i=i\pi/2$ ，于是 $i^i$ 按 $e^{i\log i}$ 计算，指数变成实数 $-\pi/2$ 。右图的半圈是几何参照，不是 $i^i$ 的输出位置；本窗口演示辐角与分支，实际幂值需要用指数定义计算。选定分支后，再给出一个确定数值才具有明确含义。

03每多记一圈，结果都会改变

取其他对数分支时， $\log i=i(\pi/2+2k\pi)$ ，相应幂值为 $e^{-\pi/2-2k\pi}$ 。它们都是正实数，但彼此不同。因此“它是实数”并不意味着“没有分支选择”；给出一个数值答案前，必须明确采用主值还是多值约定。

5.10.1 幂运算先需要一个定义¶

实数正底数的幂可以写成 $a^b=\exp(b\ln a)$ 。把底数扩展到复数，首先要解决复对数的问题。复指数绕整圈回到同一点，因此 $\mathrm i$ 对应角度 $\pi/2+2\pi k$ ，而非只有一个角度。

选择其中一个对数值 $\log\mathrm i=\mathrm i(\pi/2+2\pi k)$ ，再乘以指数 $\mathrm i$ ，得到实数 $-(\pi/2+2\pi k)$ 。对它取指数，结果便是正实数。所谓“虚数的虚数次方是实数”，关键并非神秘抵消，而是两次乘 $\mathrm i$ 带来负号。

5.10.2 主值是约定，多值是结构¶

选择主对数对应 $k=0$ ，得到 $\mathrm e^{-\pi/2}$ 。允许所有分支，则得到一族正实值。两种说法都能使用，但必须说明当前约定；不能先采用多值对数，再在计算中悄悄把它当唯一函数。

幂的复合规则也因此需要谨慎。实数正底数下熟悉的某些恒等式，推广后可能因为中间重新选取分支而失败。每次消去指数与对数之前，都应检查是否丢失整圈信息。

请把推导分成三行：选对数值、乘指数、再取指数函数。这样每一步都有明确对象与约定，也能看见 Lean 验证的是其中的代数核心，而不是建立一个没有分支问题的全局复数幂系统。

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

数学表述 5.10.1¶

复数幂通过复对数定义。复对数记录角度，而角度相差整圈时对应相同复数，因此必须指定分支。

$\log\mathrm{i}=\mathrm{i}(\pi/2+2\pi k)$ ， $k\in\mathbb Z$ 。于是多值解释下 $\mathrm{i}^{\mathrm{i}}=\exp\bigl[-(\pi/2+2\pi k)\bigr].$ 选择主对数时 $k=0$ ，主值为 $\mathrm{e}^{-\pi/2}\approx0.20788$ 。

例 5.10.1 把概念用于具体计算

关键代数是 $\mathrm{i}\cdot(\mathrm{i}\theta)=-\theta$ ，使指数变成实数。不同 $k$ 给出不同正实值，而非单个必然唯一的答案。

练习 5.10.1¶

主值 $\mathrm{i}^{2\mathrm{i}}$ 是多少？

展开解答与检查

$\mathrm{e}^{-\pi}$ ，使用相同主对数定义。

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

验证任意实角度的关键指数恒等式 $\mathrm{i}(\theta\mathrm{i})=-\theta$ ；并未将多值复幂误写成全局单值定理。

Lockdown.i_log_branch_exponent

theorem i_log_branch_exponent (θ : ℝ) :
    Complex.I*((θ:ℂ)*Complex.I)=-(θ:ℂ) := by
  calc
    Complex.I*((θ:ℂ)*Complex.I) = (θ:ℂ)*(Complex.I*Complex.I) := by ring
    _ = -(θ:ℂ) := by simp

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

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

写清选择的复对数分支，再进行指数运算，追踪整圈角度的信息。

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

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