编辑“︁Lean实数”︁

= Lean实数 =

== 介绍 ==
'''Lean实数'''是Lean定理证明器中对实数（Real Numbers）的形式化实现。在数学基础中，实数包含所有有理数和无理数，构成连续统的核心结构。Lean通过其数学库（如mathlib）提供了严格的实数定义和完备的操作体系，使程序员和数学家能够以形式化方式验证实数相关定理。

在Lean中，实数被构造为[[柯西序列]]（Cauchy sequences）或[[戴德金分割]]（Dedekind cuts）的等价类，这保证了其逻辑严密性。对于程序员而言，Lean实数不仅支持常规算术运算，还提供分析学工具（如极限、导数、积分）。

== 定义与构造 ==
Lean中实数的核心定义基于以下结构（来自mathlib）：
<syntaxhighlight lang="lean">
import data.real.basic

-- ℝ 是Lean中实数的类型
def sample_real : ℝ := 3.1415926535
</syntaxhighlight>

关键构造原理：
* '''公理化定义'''：满足[[实数公理]]（有序域完备性）。
* '''计算实现'''：依赖底层类型系统，支持精确计算与符号运算。

=== 等价构造对比 ===
<mermaid>
flowchart LR
    A[有理数 ℚ] -->|柯西序列| B(实数 ℝ)
    A -->|戴德金分割| B
    B --> C[完备性定理]
</mermaid>

== 基本操作 ==
=== 算术运算 ===
<syntaxhighlight lang="lean">
-- 加法示例
example : ℝ := 2 + 2  -- 结果为 4

-- 乘法与平方根
example : ℝ := √2 * √2  -- 结果为 2
</syntaxhighlight>

=== 不等式与绝对值 ===
<syntaxhighlight lang="lean">
lemma abs_property (x : ℝ) : |x| ≥ 0 :=
abs_nonneg x
</syntaxhighlight>

== 分析学应用 ==
=== 极限与连续性 ===
Lean可形式化验证极限定义：
<math>\lim_{x \to a} f(x) = L \iff \forall \epsilon > 0, \exists \delta > 0, |x - a| < \delta \implies |f(x) - L| < \epsilon</math>

对应代码：
<syntaxhighlight lang="lean">
import analysis.calculus.limits

example (f : ℝ → ℝ) (a L : ℝ) :
  tendsto f (𝓝 a) (𝓝 L) ↔
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| < δ → |f x - L| < ε :=
metric.tendsto_nhds_nhds
</syntaxhighlight>

=== 微分与积分 ===
<syntaxhighlight lang="lean">
import analysis.calculus.deriv

-- 导数计算
example : deriv (λ x, x^2) = λ x, 2 * x :=
by { apply deriv_pow, norm_num }
</syntaxhighlight>

== 实际案例 ==
=== 验证平方根性质 ===
证明√2是无理数：
<syntaxhighlight lang="lean">
import data.real.irrational

theorem sqrt_two_irrational : irrational (√2) :=
irrational_sqrt_two
</syntaxhighlight>

=== 工程近似计算 ===
使用泰勒级数近似e的数值：
<syntaxhighlight lang="lean">
import analysis.special_functions.exp

-- e ≈ 2.718281828459045
example : ℝ := real.exp 1
</syntaxhighlight>

== 常见问题 ==
=== 精度处理 ===
Lean区分精确实数与浮点近似：
<syntaxhighlight lang="lean">
-- 精确计算
example : (√2)^2 = 2 := by simp

-- 浮点近似（需转换）
example : float.sqrt 2.0 ^ 2 ≈ 2.0 :=
by { norm_num, apply float.sqrt_approx }
</syntaxhighlight>

=== 计算效率 ===
符号运算（如<code>√2</code>）保持精确性，而数值方法（如牛顿迭代）需显式声明近似需求。

== 扩展阅读 ==
* 实数完备性定理（Bolzano-Weierstrass、Heine-Borel等）
* Lean中的[[拓扑空间]]形式化
* 非标准分析（hyperreals）的替代实现

== 总结 ==
Lean实数系统为形式化数学提供了可靠基础，其特点包括：
* '''严格性'''：基于公理化集合论或类型论
* '''可操作性'''：与编程语言无缝集成
* '''可扩展性'''：支持高阶分析学构造

通过结合数学理论与计算实践，Lean使实数操作既可用于教育演示，也能胜任前沿研究验证。

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