これは Lean 4 Advent Calendar 2025 の4日目の記事です。
はじめに
多くの人が高校数学や大学初年度の解析学で出会う相加相乗平均の不等式（AM-GM不等式）。この有名な不等式は、多くの場合、解析学的なテクニックや凸関数を用いて証明されます。しかし、その根底には、私たちが普段使っている実数という数の体系が持つ、美しく整合性の取れた代数的な構造があります。
この記事では、証明支援系Lean4を用いて、AM-GM不等式の証明を「代数学」というレンズを通して覗いてみます。Lean4の力を借りることで、証明の各ステップが実数体のどのような性質に基づいているのかを、一つひとつ確認しながら進めることができます。
AM-GM不等式の根底にある代数学
AM-GM不等式がなぜ成り立つのか。その核心は、実数体が**順序体（ordered field）**であるという事実にあります。これは、実数の間には大小関係（順序）が定まっており、その順序が足し算や掛け算（体の演算）と非常にうまく調和している、ということを意味します。
具体的には、AM-GM不等式の証明は、実数体が持つ以下の基本的な性質に深く依存しています。
-
順序体性質: 実数の大小関係は全順序を満たし、加法・乗法と整合的です。例えば、
a < bならa + c < b + cとなります。 - 乗法の単調性: 正の数同士の乗法では、順序が保たれます。
- 平方根の存在: 負でない実数には、必ずその平方根が存在します。
-
平方の非負性: 任意の実数
xに対して、その2乗x^2は必ず0以上になります。x^2 ≥ 0という、この単純な事実が証明の出発点となります。
特に2変数の場合、a, b ≥ 0 に対して (√a - √b)^2 ≥ 0 という自明な不等式を展開し、整理するだけで、AM-GM不等式 (a+b)/2 ≥ √ab が魔法のように現れます。この導出プロセス全体が、まさに実数体の代数的な性質そのものなのです。
Lean4による2変数AM-GM不等式の形式的証明
それでは、この代数的な証明の道のりをLean4で実際に辿ってみましょう。以下に示すコードは、Lean4の数学ライブラリMathlibをインポートした上で、2変数のAM-GM不等式とその等号成立条件を証明するものです。
Lean4コード全体
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Tactic
/-!
# 相加相乗平均の不等式 (AM-GM Inequality)
-/
namespace AMGMProofs
/-! ## 1. 代数学的な準備（実数の順序体の性質） -/
/-- **補題 1.1**: 実数の平方は常に非負である。 -/
theorem square_nonneg (x : ℝ) : 0 ≤ x^2 := by
exact sq_nonneg x
/-- **補題 1.2**: 非負実数の平方根の平方は元の数に等しい。 -/
theorem sqrt_sq_eq_self {x : ℝ} (hx : 0 ≤ x) : (Real.sqrt x)^2 = x := by
exact Real.sq_sqrt hx
/-! ## 2. 2変数の場合のAM-GM不等式 -/
/--
**定理 2.2**: 2変数AM-GM不等式
2つの非負実数 `a`, `b` に対して、その相加平均は相乗平均以上である。
-/
theorem am_gm_two_vars (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) :
Real.sqrt (a * b) ≤ (a + b) / 2 := by
-- 証明の出発点として、(√a - √b)² ≥ 0 を利用する
-- これは、平方の非負性(square_nonneg)から自明
have h_base : 0 ≤ (Real.sqrt a - Real.sqrt b)^2 := by
exact square_nonneg (Real.sqrt a - Real.sqrt b)
-- (√a - √b)² を展開する: (√a)² - 2√a√b + (√b)²
have h_expand : (Real.sqrt a - Real.sqrt b)^2 = (Real.sqrt a)^2 - 2 * Real.sqrt a * Real.sqrt b + (Real.sqrt b)^2 := by
ring -- 環(ring)の公理に基づいて式を展開するタクティク
-- 展開した式を h_base に適用する
rw [h_expand] at h_base
-- (√x)² = x の性質と、√a * √b = √(a * b) の性質を使って式を簡単化する
rw [sqrt_sq_eq_self ha, sqrt_sq_eq_self hb, Real.sqrt_mul ha] at h_base
-- これで `0 ≤ a - 2 * Real.sqrt (a * b) + b` が得られた
-- 不等式を整理して、目的の形に変形する (線形算術で解く)
-- `2 * Real.sqrt (a * b) ≤ a + b` と同値
have h_rearranged : 2 * Real.sqrt (a * b) ≤ a + b := by
linarith [h_base]
-- 両辺を2で割る。2は正の数なので不等号の向きは変わらない
-- `Real.sqrt (a * b) ≤ (a + b) / 2`
exact (div_le_iff' (by norm_num)).mpr h_rearranged
/-! ## 3. 等号成立条件 -/
/--
**定理 3.1**: 2変数AM-GM不等式の等号成立条件
2つの非負実数 `a`, `b` に対して、相加平均と相乗平均が等しくなるのは `a = b` のとき、かつそのときに限る。
-/
theorem am_gm_two_vars_iff_eq (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) :
Real.sqrt (a * b) = (a + b) / 2 ↔ a = b := by
constructor
-- `sqrt(a*b) = (a+b)/2` ならば `a=b` であることを示す (→方向)
· intro h_eq
-- 証明の流れ: `h_eq`から逆算して `(√a - √b)² = 0` を導き、`√a = √b` から `a = b` を示す
have h1 : 2 * Real.sqrt (a * b) = a + b := by linarith [(div_eq_iff (by norm_num)).mp h_eq]
rw [Real.sqrt_mul ha] at h1
have h2 : a - 2 * Real.sqrt a * Real.sqrt b + b = 0 := by linarith [h1]
have h3 : (Real.sqrt a - Real.sqrt b)^2 = 0 := by
rw [sub_sq (Real.sqrt a) (Real.sqrt b)]
rw [sqrt_sq_eq_self ha, sqrt_sq_eq_self hb]
exact h2
have h4 : Real.sqrt a - Real.sqrt b = 0 := by exact sq_eq_zero_iff.mp h3
have h5 : Real.sqrt a = Real.sqrt b := by linarith [h4]
-- 両辺を2乗して a = b を得る
exact (Real.sqrt_inj ha hb).mp h5
-- `a=b` ならば `sqrt(a*b) = (a+b)/2` であることを示す (←方向)
· intro h_eq
-- a = b を代入すれば自明
rw [h_eq]
-- `sqrt(b*b) = (b+b)/2` を示す
rw [← Real.sqrt_mul_self hb] -- sqrt(b*b) = b (b>=0)
rw [add_self_div_two]
end AMGMProofs
証明の解説
-
am_gm_two_vars: 2変数AM-GM不等式の本体です。証明の出発点は、コメントにある通り(√a - √b)^2 ≥ 0という事実です。Leanのコードではsquare_nonnegというMathlibに既にある定理を利用しています。 -
ringタクティク:(√a - √b)^2を展開する際にringというタクティクが登場します。これは、式が環の公理（分配法則や結合法則など、まさに代数学の基本ルール）に従って変形できることを自動で検証・実行してくれます。 -
linarithタクティク: 式の移項や整理にはlinarith（linear arithmetic）というタクティクが活躍します。これも、順序体の線形な不等式に関する代数的な推論を自動で行ってくれる強力なツールです。 -
am_gm_two_vars_iff_eq: 等号成立条件(a+b)/2 = √ab ⇔ a = bを証明しています。証明のロジックは、手計算で行う代数的な式変形と全く同じです。Leanがその変形の正しさを厳密にチェックしてくれます。
このように、Lean4の証明は、私たちが手で計算する際の思考プロセスを非常に忠実に再現しており、かつ、その一行一行が厳密な代数的ルールに基づいていることを保証してくれます。
n変数の場合への展望
今回は最も単純な2変数の場合を取り上げましたが、この代数的な視点は、より一般的なn変数のAM-GM不等式の証明にも繋がっていきます。n変数の証明は数学的帰納法などを用いて行われますが、その各ステップもまた、ここで利用したような代数的な性質が基礎となっています。
ちなみに、Leanの数学ライブラリMathlibには、n変数のAM-GM不等式もReal.geom_mean_le_arith_meanという名前で既に実装されています。興味のある方は、その定義や証明を追ってみると、より深い理解が得られるでしょう。
おわりに
本記事では、相加相乗平均の不等式という解析学的な題材を、Lean4を使ってその代数的な側面から掘り下げてみました。証明支援系を用いることで、数学的な定理の根底にある構造をより明確に意識し、楽しみながら学ぶことができます。
明日は、Lean 4 Advent Calendar 2025 の5日目です。お楽しみに！