编辑“︁Lean复数”︁（章节）

= Lean复数 =

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

== 复数的定义 ==

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

=== Lean中的复数类型 ===
Lean的 `Complex` 类型定义如下：
<syntaxhighlight lang="lean">
structure Complex where
  re : ℝ  -- 实部
  im : ℝ  -- 虚部
</syntaxhighlight>

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

== 复数的基本运算 ==

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

=== 示例：复数的构造与运算 ===
<syntaxhighlight lang="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
</syntaxhighlight>

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

== 复数的性质与函数 ==

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

=== 示例：复数的模与指数函数 ===
<syntaxhighlight lang="lean">
-- 计算复数的模（绝对值）
#eval Complex.abs z1  -- 输出：5（因为 √(3² + 4²) = 5）

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

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

== 实际应用案例 ==

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

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

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

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

解释：
* 旋转后的复数计算为 <math>e^{i\pi/2} \cdot (1 + i) = i \cdot (1 + i) = -1 + i</math>。
* 结果 <math>-1 + 1i</math> 对应于旋转后的点 <math>(-1, 1)</math>。

== 可视化复数 ==

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

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

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

== 总结 ==

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

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

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean数学基础]]