Real, NNReal, EReal, ENNReal: 実数系の型

数学では実数の構成として，Dedekind cut，Cauchy 列による完備化，完備順序体としての公理化など，いくつかの標準的な方法があります． Mathlib の Real は，実装上は有理数の Cauchy 列の同値類として構成されています． ただし，通常の形式化ではこの構成を直接展開することはほとんどありません． 実用上は，ℝ が体，線形順序，位相空間，完備距離空間，条件付き完備線形順序などの構造を持つ型である，というインターフェースを使います．

プログラミング言語の Float とも違います． Lean の ℝ は有限精度の浮動小数点数ではなく，証明対象としての数学的な実数です． 丸め誤差を含む計算ではなく，定理として a + b = b + a や中間値の定理，完備性などを扱うための型です．

Mathlib.Data 配下には，実数そのものに加えて，非負実数や拡張実数を表す型が用意されています．

型	notation	構成	主な用途
Real	ℝ	有理数 Cauchy 列の同値類	通常の実解析，代数，位相
NNReal	ℝ≥0	{r : ℝ // 0 ≤ r}	非負量，距離，ノルム，確率など
ENNReal	ℝ≥0∞	WithTop ℝ≥0	測度，拡張距離，∞ を許す非負量
EReal	なし	WithBot (WithTop ℝ)	[-∞, ∞] 型の拡張実数，limsup/liminf など

名前だけ見ると似ていますが，これらは別々の型です． 型が違うものを混ぜるときは，coercion や toReal，ofReal，toNNReal などの変換を確認します． 特に，toReal や ofReal には情報を失うものがあります．

#check Real
#check ℝ
#check NNReal
#check ℝ≥0
#check ENNReal
#check ℝ≥0∞
#check EReal

#synth Field ℝ
#synth LinearOrder ℝ
#synth IsStrictOrderedRing ℝ
#synth Archimedean ℝ
#synth TopologicalSpace ℝ
#synth CompleteSpace ℝ
#synth ConditionallyCompleteLinearOrder ℝ

#synth LinearOrderedCommGroupWithZero ℝ≥0
#synth ConditionallyCompleteLinearOrderBot ℝ≥0
#synth CompleteLinearOrder ℝ≥0∞
#synth CompleteLinearOrder EReal

#check Real.equivCauchy
#check Real.sqrt
#check Real.sqrt_sq_eq_abs

example : ((3 : Nat) : ℝ) + 2 = 5 := by
  norm_num

example (x : ℝ) : 0 ≤ |x| := by
  exact abs_nonneg x

example (x : ℝ) : Real.sqrt (x ^ 2) = |x| := by
  simpa using Real.sqrt_sq_eq_abs x

norm_num は数値計算に強い tactic です． 実数上の具体的な数値等式・不等式を閉じるときによく使います． Real.sqrt のような標準関数も Real 名前空間に置かれ，補題名も Real.sqrt_sq_eq_abs のように整理されています．

NNReal: 非負実数

NNReal は nonnegative real，つまり \([0, \infty)\) に対応する型です． notation は ℝ≥0 です． 実装は ℝ の subtype で，

Mathlib.Data.NNReal.Defs

def NNReal := { r : ℝ // 0 ≤ r }

です． 要素は実数 r と証明 0 ≤ r の組ですが，通常は coercion により実数としても使えます． NNReal.mk x hx は，非負性の証明 hx : 0 ≤ x から x : ℝ≥0 を作るコンストラクタです． 一方，Real.toNNReal x は任意の実数を非負実数に送りますが，負の値は 0 に潰します． したがってこれは単なる型変換ではありません．

#check NNReal.mk
#check NNReal.toReal
#check Real.toNNReal
#check Real.coe_toNNReal
#check Real.toNNReal_of_nonpos

example (x : ℝ≥0) : (0 : ℝ) ≤ (x : ℝ) := by
  exact x.property

example (x : ℝ) (hx : 0 ≤ x) : ((Real.toNNReal x : ℝ≥0) : ℝ) = x := by
  exact Real.coe_toNNReal x hx

example : ((Real.toNNReal (-3 : ℝ) : ℝ≥0) : ℝ) = 0 := by
  norm_num [Real.toNNReal]

ℝ≥0 は非負性を型に持たせたいときに便利です． たとえば距離，ノルム，確率，非負関数などは，値が常に非負であることを命題として毎回仮定するより，値域を ℝ≥0 にすると扱いやすくなります． ただし，ℝ≥0 は体ではありません． 負数を持たないので，通常の ℝ と同じ引き算・反数の感覚で使うと詰まります．

ENNReal: 拡張非負実数

ENNReal は extended nonnegative real，つまり \([0, \infty]\) に対応する型です． notation は ℝ≥0∞ で，実装は WithTop ℝ≥0 です． これは ℝ≥0 に新しい最大元 ∞ を付け加えた型です．

測度論では，測度や非負関数の積分値が ∞ になりうるため，ENNReal がよく現れます． また，拡張距離 edist の値域としても使われます． ENNReal には ∞ があるため，toReal は ∞ を 0 に送ります． また，ENNReal.ofReal は負の実数を 0 に送ります． したがって，toReal と ofReal は情報を失う変換です．

#check ENNReal.ofReal
#check ENNReal.toReal
#check ENNReal.toNNReal
#check ENNReal.ofReal_ne_top
#check ENNReal.toReal_ofReal

example : (0 : ℝ≥0∞) ≤ ∞ := by
  simp

example : (∞ : ℝ≥0∞) + 1 = ∞ := by
  simp

example : (1 : ℝ≥0∞) + 2 = 3 := by
  norm_num

example : ENNReal.ofReal (-3 : ℝ) = 0 := by
  norm_num [ENNReal.ofReal, Real.toNNReal]

example (x : ℝ) (hx : 0 ≤ x) : (ENNReal.ofReal x).toReal = x := by
  exact ENNReal.toReal_ofReal hx

example : (∞ : ℝ≥0∞).toReal = 0 := by
  rfl

ENNReal.ofReal x は常に有限な ℝ≥0∞ です． そのため ENNReal.ofReal_ne_top のような補題があります． 一方で，∞ から ℝ に戻すと 0 になるので，toReal を使うときは有限性の仮定 a ≠ ∞ が必要になることが多いです．

EReal: 符号つき拡張実数

EReal は extended real，つまり \([-\infty, \infty]\) に対応する型です． 実装は WithBot (WithTop ℝ) で，ℝ に上端 ⊤ と下端 ⊥ を追加したものです． ENNReal が非負側だけを拡張するのに対し，EReal は正負両方向に無限大を持ちます．

EReal は完備線形順序として扱えるため，順序論的な上限・下限や limsup/liminf のように，正負の無限大が自然に出る場面で使います． ただし，代数演算には通常の実数とは違う注意点があります． たとえば EReal.toReal も ⊤ と ⊥ を 0 に送ります．

#check EReal
#check EReal.toReal
#check EReal.toReal_top
#check EReal.toReal_bot
#check EReal.toReal_coe

example : EReal.toReal (⊤ : EReal) = 0 := by
  exact EReal.toReal_top

example : EReal.toReal (⊥ : EReal) = 0 := by
  exact EReal.toReal_bot

example (x : ℝ) : EReal.toReal (x : EReal) = x := by
  exact EReal.toReal_coe x

まとめると，通常の実解析ではまず ℝ を使います． 値が非負であることを型に持たせたいなら ℝ≥0，非負で ∞ も許したいなら ℝ≥0∞，正負両方の無限大を許したいなら EReal を使います． 変換関数の名前を見たら，それが埋め込みなのか，負の値や無限大を 0 に潰す写像なのかを確認するのが重要です．

演習

Real，NNReal，ENNReal，EReal の型と変換を確認してください．

#check Real
#check NNReal
#check ENNReal
#check EReal
#synth TopologicalSpace ℝ
#synth ConditionallyCompleteLinearOrder ℝ
#synth CompleteLinearOrder ℝ≥0∞
#synth CompleteLinearOrder EReal

example (x : ℝ) (hx : 0 ≤ x) :
    ((Real.toNNReal x : ℝ≥0) : ℝ) = x := by
  -- 解答例:
  --   exact Real.coe_toNNReal x hx
  sorry

example : ENNReal.ofReal (-3 : ℝ) = 0 := by
  -- 解答例:
  --   exact ENNReal.ofReal_of_nonpos (by norm_num)
  sorry