Lean向量空间
Lean向量空间是数学中线性代数的核心概念在Lean定理证明器中的形式化实现。它描述了满足特定公理（加法交换律、标量乘法分配律等）的数学结构，为程序员提供严格的代数工具。本文将从基础定义逐步深入到形式化实现，适合从初学者到高级用户的不同需求。
数学定义[编辑 | 编辑源代码]
在经典数学中，向量空间（或称线性空间）是定义在域上的集合，配备两种运算：
- 向量加法：
- 标量乘法：
满足以下公理：
Lean中的形式化[编辑 | 编辑源代码]
在Lean中，向量空间通过类型类`vector_space`实现（以Mathlib库为例）：
import algebra.module.basic
variables (𝕜 : Type*) [field 𝕜] (V : Type*) [add_comm_group V] [module 𝕜 V]
-- 自动继承module结构即定义向量空间
example : vector_space 𝕜 V := by apply_instance
关键组件说明：
- `𝕜`表示标量域（如ℝ或ℂ）
- `V`表示向量类型
- `add_comm_group`提供加法交换群结构
- `module`包含标量乘法运算
基础操作示例[编辑 | 编辑源代码]
-- 定义实数向量空间
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]
可视化理解[编辑 | 编辑源代码]
实际应用案例[编辑 | 编辑源代码]
图形变换[编辑 | 编辑源代码]
在计算机图形学中，二维/三维向量空间用于表示顶点坐标。通过矩阵（线性映射）实现旋转、缩放：
-- 二维旋转矩阵
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)
机器学习[编辑 | 编辑源代码]
参数空间作为向量空间的典型应用：
-- 定义权重向量空间
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 }
进阶主题[编辑 | 编辑源代码]
子空间验证[编辑 | 编辑源代码]
在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]⟩
商空间构造[编辑 | 编辑源代码]
-- 给定子空间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
常见问题[编辑 | 编辑源代码]
总结[编辑 | 编辑源代码]
Lean向量空间将抽象代数与程序验证结合，其形式化特性使得：
- 数学证明可执行验证
- 算法实现附带正确性保证
- 抽象层次可扩展（如希尔伯特空间）