Lean复数

Lean复数

复数（Complex Numbers）是数学中一类重要的数，由实数部分和虚数部分组成，在工程、物理和计算机科学中有广泛应用。在Lean中，复数被定义为一种结构体，包含实部（re）和虚部（im）。本章将介绍如何在Lean中定义和使用复数，并展示其基本运算和应用。

复数的定义

在数学中，复数通常表示为 $a+bi$，其中 $a$ 是实部，$b$ 是虚部，$i$ 是虚数单位，满足 $i^2=-1$。在Lean中，复数可以通过标准库 `Mathlib` 中的 `Complex` 类型来使用。

Lean中的复数类型

Lean的 `Complex` 类型定义如下：

structure Complex where
  re : ℝ  -- 实部
  im : ℝ  -- 虚部

这里，`ℝ` 表示实数类型，`re` 和 `im` 分别存储复数的实部和虚部。

复数的基本运算

Lean提供了复数的基本运算，包括加法、减法、乘法和除法。以下示例展示了如何在Lean中定义和操作复数。

示例：复数的构造与运算

import Mathlib.Data.Complex.Basic

-- 定义两个复数
def z1 : ℂ := ⟨3, 4⟩  -- 3 + 4i
def z2 : ℂ := ⟨1, -2⟩ -- 1 - 2i

-- 复数加法
#eval z1 + z2  -- 输出：4 + 2i

-- 复数乘法
#eval z1 * z2  -- 输出：11 - 2i

-- 复数共轭
#eval Complex.conj z1  -- 输出：3 - 4i

解释：

• `z1 + z2` 计算为 $(3+1)+(4-2)i=4+2i$。
• `z1 * z2` 计算为 $(3\cdot 1-4\cdot (-2))+(3\cdot (-2)+4\cdot 1)i=11-2i$。
• `Complex.conj z1` 返回复数的共轭复数，即实部不变，虚部取反。

复数的性质与函数

复数支持许多数学函数，如模（绝对值）、指数函数和对数函数。以下示例展示了一些常见操作：

示例：复数的模与指数函数

-- 计算复数的模（绝对值）
#eval Complex.abs z1  -- 输出：5（因为 √(3² + 4²) = 5）

-- 计算复数的指数函数
#eval Complex.exp (⟨0, π⟩ : ℂ)  -- 输出：-1（欧拉公式 e^(iπ) = -1）

解释：

• `Complex.abs z1` 计算复数的模，即 $\sqrt{3^2+4^2}=5$。
• `Complex.exp (⟨0, π⟩)` 应用欧拉公式 $e^{i\pi }=-1$。

实际应用案例

复数在信号处理、量子计算和图形学中有广泛应用。以下是一个简单的案例，展示如何在Lean中使用复数进行二维旋转：

案例：复数表示二维旋转

二维平面上的点 $(x,y)$ 可以表示为复数 $x+yi$。旋转角度 $\theta$ 可以通过乘以 $e^{i\theta }$ 实现：

-- 定义旋转函数
def rotate (θ : ℝ) (z : ℂ) : ℂ := Complex.exp (⟨0, θ⟩) * z

-- 旋转90度（π/2弧度）
def point : ℂ := ⟨1, 1⟩  -- 点 (1, 1)
#eval rotate (π / 2) point  -- 输出：-1 + 1i

解释：

• 旋转后的复数计算为 $e^{i\pi /2}\cdot (1+i)=i\cdot (1+i)=-1+i$。
• 结果 $-1+1i$ 对应于旋转后的点 $(-1,1)$。

可视化复数

可以使用Mermaid图表展示复数的几何表示：

graph LR A[原点] --> B[复数 z = 3 + 4i] B --> C[实轴: 3] B --> D[虚轴: 4] B --> E[模: 5]

该图展示了复数 $3+4i$ 在复平面上的表示，包括实部、虚部和模。

总结

本章介绍了Lean中复数的定义、基本运算和实际应用。复数在数学和工程中非常重要，Lean的 `Mathlib` 提供了丰富的支持。通过代码示例和案例，我们展示了如何在Lean中使用复数进行计算和几何变换。

下一步，可以学习复数的更高级应用，如傅里叶变换或量子计算中的复数运算。