编辑“︁Lean向量空间”︁

{{DISPLAYTITLE:Lean向量空间}}

'''Lean向量空间'''是[[数学]]中[[线性代数]]的核心概念在[[Lean定理证明器]]中的形式化实现。它描述了满足特定公理（加法交换律、标量乘法分配律等）的数学结构，为程序员提供严格的代数工具。本文将从基础定义逐步深入到形式化实现，适合从初学者到高级用户的不同需求。

== 数学定义 ==
在经典数学中，向量空间<math>V</math>（或称线性空间）是定义在[[域]]<math>\mathbb{F}</math>上的集合，配备两种运算：
* '''向量加法'''：<math>+ : V \times V \to V</math>
* '''标量乘法'''：<math>\cdot : \mathbb{F} \times V \to V</math>

满足以下公理：
<math display="block">
\begin{align}
&\text{1. 加法交换律} & \mathbf{u} + \mathbf{v} &= \mathbf{v} + \mathbf{u} \\
&\text{2. 加法结合律} & (\mathbf{u} + \mathbf{v}) + \mathbf{w} &= \mathbf{u} + (\mathbf{v} + \mathbf{w}) \\
&\text{3. 标量乘法结合律} & a(b\mathbf{v}) &= (ab)\mathbf{v} \\
&\text{4. 分配律} & a(\mathbf{u} + \mathbf{v}) &= a\mathbf{u} + a\mathbf{v} \\
&\text{5. 单位元存在} & \exists \mathbf{0} \in V, \forall \mathbf{v} \in V, \mathbf{0} + \mathbf{v} &= \mathbf{v}
\end{align}
</math>

== Lean中的形式化 ==
在Lean中，向量空间通过类型类`vector_space`实现（以Mathlib库为例）：

<syntaxhighlight lang="lean">
import algebra.module.basic

variables (𝕜 : Type*) [field 𝕜] (V : Type*) [add_comm_group V] [module 𝕜 V]

-- 自动继承module结构即定义向量空间
example : vector_space 𝕜 V := by apply_instance
</syntaxhighlight>

关键组件说明：
* `𝕜`表示标量域（如ℝ或ℂ）
* `V`表示向量类型
* `add_comm_group`提供加法交换群结构
* `module`包含标量乘法运算

=== 基础操作示例 ===
<syntaxhighlight lang="lean">
-- 定义实数向量空间
example : vector_space ℝ (ℝ × ℝ) := by apply_instance

-- 向量加法和标量乘法演示
def vec_add : ℝ × ℝ → ℝ × ℝ → ℝ × ℝ := λ v w, (v.1 + w.1, v.2 + w.2)
def scalar_mul : ℝ → ℝ × ℝ → ℝ × ℝ := λ a v, (a * v.1, a * v.2)

-- 验证分配律
lemma distrib (a : ℝ) (v w : ℝ × ℝ) : 
  scalar_mul a (vec_add v w) = vec_add (scalar_mul a v) (scalar_mul a w) :=
by simp [vec_add, scalar_mul]
</syntaxhighlight>

== 可视化理解 ==
<mermaid>
graph LR
    A[向量空间] --> B[加法封闭性]
    A --> C[标量乘法封闭性]
    B --> D[交换律/结合律]
    C --> E[分配律/结合律]
    A --> F[零向量存在]
</mermaid>

== 实际应用案例 ==
=== 图形变换 ===
在计算机图形学中，二维/三维向量空间用于表示顶点坐标。通过矩阵（线性映射）实现旋转、缩放：

<syntaxhighlight lang="lean">
-- 二维旋转矩阵
def rotation_matrix (θ : ℝ) : matrix (fin 2) (fin 2) ℝ :=
![![cos θ, -sin θ], ![sin θ, cos θ]]

-- 矩阵作用于向量（线性变换）
def rotate_vec (θ : ℝ) (v : ℝ × ℝ) : ℝ × ℝ :=
  (cos θ * v.1 - sin θ * v.2, sin θ * v.1 + cos θ * v.2)
</syntaxhighlight>

=== 机器学习 ===
参数空间作为向量空间的典型应用：

<syntaxhighlight lang="lean">
-- 定义权重向量空间
structure neural_net (input_dim : ℕ) :=
(weights : fin input_dim → ℝ)  -- 权重向量
(bias : ℝ)                     -- 偏置项

-- 梯度下降步骤即向量空间中的加法
def gradient_step (η : ℝ) (grad : neural_net n) (net : neural_net n) : neural_net n :=
{ weights := λ i, net.weights i - η * grad.weights i,
  bias := net.bias - η * grad.bias }
</syntaxhighlight>

== 进阶主题 ==
=== 子空间验证 ===
在Lean中证明子集构成子空间：

<syntaxhighlight lang="lean">
def is_subspace (s : set V) : Prop :=
0 ∈ s ∧ (∀ v w ∈ s, v + w ∈ s) ∧ (∀ c : 𝕜, ∀ v ∈ s, c • v ∈ s)

-- 例如：零子空间
lemma zero_subspace : is_subspace 𝕜 V ({0} : set V) :=
⟨by simp, by simp, λ c v hv, by simp [hv]⟩
</syntaxhighlight>

=== 商空间构造 ===
<syntaxhighlight lang="lean">
-- 给定子空间W构造商空间V/W
def quotient_space (W : submodule 𝕜 V) := V ⧸ W

-- 商投影保持线性结构
lemma quotient_linear (f : V →ₗ[𝕜] V') (h : W ≤ f.ker) : 
  ∃ g : quotient_space W →ₗ[𝕜] V', g ∘ quotient.mk = f :=
quotient.lift_linear _ h
</syntaxhighlight>

== 常见问题 ==
{{Q&A
|问题=为什么需要形式化向量空间？
|回答=严格验证算法（如神经网络训练）的数学正确性，避免浮点运算误差累积导致的理论缺陷。
}}
{{Q&A
|问题=如何处理无限维空间？
|回答=通过类型系统参数化（如`ι → ℝ`表示基的线性组合），需额外假设选择公理。
}}

== 总结 ==
Lean向量空间将抽象代数与程序验证结合，其形式化特性使得：
* 数学证明可执行验证
* 算法实现附带正确性保证
* 抽象层次可扩展（如希尔伯特空间）

通过持续探索Mathlib中的`linear_algebra`库，用户可以深入更高级的应用如[[张量积]]或[[谱理论]]的形式化。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean代数结构]]