Zenn
😸

Lean4でのHoeffding不等式の証明

に公開
lean4
不等式
tech

PAC-baysの証明などで登場する確率分布の不等式の一つHoeffdingの不等式の証明
使用例
https://joisino.hatenablog.com/entry/theory

ベースはChatGPT5
https://chatgpt.com/share/68a3be0e-c068-8008-9cdc-fb8087c3490f

主張

確率変数Xに対して

Pr[\frac{1}{n}\sum_{i=0}^n (X_i-E[X_i])\le t)] \ge e^{-\frac{2n^2}{(a-b)^2}}
Pr[\frac{1}{n}\sum_{i=0}^n (X_i-E[X_i])\ge -t)]\ge e^{-\frac{2n^2}{(a-b)^2}}

https://ludu-vorton.hatenablog.com/entry/2019/06/06/073000
https://seetheworld1992.hatenablog.com/entry/2017/06/04/150253

証明スクリプト

以下は、mathlib4 に既に実装されている sub-Gaussian／Azuma–Hoeffding 系の定理を組み合わせる。

概要

  • 有界かつ平均 0 の確率変数 X に対して Hoeffding の補題
    hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero により
    X はパラメータ ((‖b - a‖₊ / 2) ^ 2) の sub-Gaussian（MGF）である。
  • 独立族 {X i} の有限和に対して sub-Gaussian の和の Chernoff/Hoeffding 上界
    measure_sum_ge_le_of_iIndepFun が使える（定数は足し合わさる）。
  • これらを合成すると「（平均 0・有界・独立）な有限個の確率変数の和」に対する Hoeffding の不等式がそのまま得られる。

有限和版

/-
Hoeffding's inequality in Lean 4 (mathlib4).
-/
import Mathlib/Probability/Moments/SubGaussian
import Mathlib/Data/Real/ENNReal
import Mathlib/MeasureTheory/Measure/ProbabilityMassFunction

open scoped BigOperators
open ProbabilityTheory

variable {Ω ι : Type*} [MeasurableSpace Ω]
variable {μ : Measure Ω}

theorem hoeffding_finset
  [IsProbabilityMeasure μ]
  (s : Finset ι) (X : ι → Ω → ℝ) (a b : ι → ℝ)
  (hMeas : ∀ i ∈ s, AEMeasurable (X i) μ)
  (hBound : ∀ i ∈ s, ∀ᵐ ω ∂μ, X i ω ∈ Set.Icc (a i) (b i))
  (hMean0 : ∀ i ∈ s, ∫ ω, X i ω ∂μ = 0)
  (hIndep : iIndepFun X μ)
  {ε : ℝ} (hε : 0 ≤ ε) :
  μ.real {ω | ε ≤ ∑ i ∈ s, X i ω}
    ≤ Real.exp(- ε^2 /(2*(↑(∑i∈ s,((‖bi - ai‖₊/2)^2 : NNReal))))) := by
  classical
  -- Each summand is sub-Gaussian with parameter (‖b-a‖₊/2)^2 (Hoeffding's lemma).
  have hSub :
      ∀ i ∈ s, HasSubgaussianMGF (X i) ((‖b i - a i‖₊ / 2) ^ 2) μ := by
    intro i hi
    exact
      hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero
        (hMeas i hi) (hBound i hi) (hMean0 i hi)
  -- Chernoff/Hoeffding for sums of independent sub-Gaussians.
  simpa using
    (HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun
      (μ := μ) (X := X) (s := s)
      (c := fun i => (‖b i - a i‖₊ / 2) ^ 2)
      hIndep hSub hε)

無限和版

/-- **Hoeffding (i.i.d.-style, common width).**
-/
theorem hoeffding_sum_range
  [IsProbabilityMeasure μ]
  (X : ℕ → Ω → ℝ) (a b : ℝ) (n : ℕ)
  (hMeas : ∀ i < n, AEMeasurable (X i) μ)
  (hBound : ∀ i < n, ∀ᵐ ω ∂μ, X i ω ∈ Set.Icc a b)
  (hMean0 : ∀ i < n, ∫ ω, X i ω ∂μ = 0)
  (hIndep : iIndepFun X μ)
  {ε : ℝ} (hε : 0 ≤ ε) :
  μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω}
    ≤ Real.exp (- ε^2 /(2 * (n : ℝ) *(↑(((‖b - a‖₊) / 2) ^ 2:NNReal)))) := by classical
  -- common sub-Gaussian parameter
  set c : NNReal := ((‖b - a‖₊ / 2) ^ 2)
  have hSub : ∀ i < n, HasSubgaussianMGF (X i) c μ := by
    intro i hi
    exact
      hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero
        (hMeas i hi) (hBound i hi) (hMean0 i hi)
  -- direct range-version bound in mathlib
  --   μ {ε ≤ ∑_{i < n} X_i} ≤ exp( - ε^2 / (2 n c) ).
  simpa [c, mul_comm, mul_left_comm, mul_assoc] using
    (HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun
      (μ := μ) (X := X) (n := n) (c := c)
      hIndep hSub hε)

スクリプト説明

主張

以下のようにコメントに書かれている

Let s:Finset ι and random variables Xi (i ∈ s) be independent,
a.s. bounded in [ai, bi], and mean-zero.
Then, for all ε ≥ 0, μ { ω | ε ≤ ∑ i∈s, Xi ω } ≤ exp(-ε^2/(2*∑i∈s ((‖bi - ai‖₊ /2)^2)) ).
This is the classical Hoeffding bound (via sub-Gaussian MGF + Chernoff).

有限集合sとランダム変数X_iに対して領域[ai,bi]があるとする。すると任意のε>=0に対して

μ{ ω | ε ≤ ∑ i∈s, Xi ω } ≤ exp(-ε^2/(2*∑i∈s ((‖bi-ai‖₊/2)^2)) )`

が成り立つというもの

使う変数の定義

variable {Ω ι : Type*} [MeasurableSpace Ω]

variable {μ : Measure Ω}

定理本体

theorem hoeffding_finset
  [IsProbabilityMeasure μ]
  (s : Finset ι) (X : ι → Ω → ℝ) (a b : ι → ℝ)
  (hMeas : ∀ i ∈ s, AEMeasurable (X i) μ)
  (hBound : ∀ i ∈ s, ∀ᵐ ω ∂μ, X i ω ∈ Set.Icc (a i) (b i))
  (hMean0 : ∀ i ∈ s, ∫ ω, X i ω ∂μ = 0)
  (hIndep : iIndepFun X μ)
  {ε : ℝ} (hε : 0 ≤ ε) :
  μ.real {ω | ε ≤ ∑ i ∈ s, X i ω}
    ≤ Real.exp(- ε^2 /(2*(↑(∑i∈ s,((‖bi - ai‖₊/2)^2 : NNReal))))) := by
  classical

仮定(型)

  • [IsProbabilityMeasure μ]
    測度空間 (Ω, μ) が確率測度（全体測度が 1）であるという型クラス

  • X : ι → Ω → ℝ
    添字集合 ι（有限部分集合 s を考える）で添字づけられた実確率変数族(Xi)。

  • hMeas : ∀ i ∈ s, AEMeasurable (X i) μ
    ほとんど至る所可測。

  • hBound : ∀ i ∈ s, ∀ᵐ ω, X i ω ∈ Set.Icc (a i) (b i)
    a.e.に[ai, bi]に入る有界性）。Icc は閉区間[ , ]。a≤bを仮定していないが、‖b-a‖₊ を使うことで向きに依らず幅だけ取り出します。

  • hMean0 : ∀ i ∈ s, ∫ ω, X i ω ∂μ = 0
    平均 0。

  • hIndep : iIndepFun X μ
    （族としての）独立性。iIndepFun は「添字族全体が相互独立」であることを表す mathlib の述語です。実際に使うのは有限和上だけですが、証明では族全体の独立性を仮定しています。

  • {ε : ℝ} (hε : 0 ≤ ε)
    Chernoff 法に必要な ε ≥ 0。

  • 結論の左辺 μ.real {ω | ε ≤ ∑ i ∈ s, X i ω}
    μの集合測度をℝ型で扱うためのμ.real（ENNRealではなくℝに落としたいときに使う補助）。

:= by classic

は古典選択公理に基づく議論

証明

  • Hoeffdingの補題 hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero
    Each summand is sub-Gaussian with parameter (‖b-a‖₊/2)^2

mathlib では HasSubgaussianMGF（積率母関数に対する上界、すなわちE[e^{tX} \le \exp(\sigma^2t^2/2)を表現し、対応する定理がhasSubgaussianMGF_of_mem_Icc_of_integral_eq_zeroなので
hMeas, hBound, hMean0をそのまま代入して各iで得ます。

  • intro
  • exact
  have hSub :
      ∀ i ∈ s, HasSubgaussianMGF (X i)((‖b i - a i‖₊/2)^2) μ := by
    intro i hi
    exact
      hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero
        (hMeas i hi) (hBound i hi) (hMean0 i hi)
  • Chernoff界　HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun
    Chernoff/Hoeffding for sums of independent sub-Gaussians.
    measure_sum_ge_le_of_iIndepFun は独立族hIndep各成分がHasSubgaussianMGF で、パラメータをc iとして与える hSub ε ≥ 0 から
    \mu( \sum_{i\in s}X_i\ge \epsilon ) \le \exe(-\frac{\epsilon^2}{2\sum_{i\in s} c(i)}
    を返す補題
    simpaは返ってきた結論がゴールと完全一致するので簡約して同一視するという意味
  simpa using
    (HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun
      (μ := μ) (X := X) (s := s)
      (c := fun i => (‖b i - a i‖₊ / 2) ^ 2)
      hIndep hSub hε)

【サンプル平均の形】

n > 0 で ε := n * t (t ≥ 0) と置くと、
{ t ≤ (1/n) * ∑ X_i } = { n*t ≤ ∑ X_i }（n が正）なので、
上の hoeffding_sum_range から

μ { ω | t ≤ ( (∑_{i<n} X_i ω) / n ) } ≤ exp( - 2 * n * t^2 / (b - a)^2 )

が従います（計算は c = (‖b-a‖₊/2)^2 を用いて 2 * n * c = (b-a)^2 / 2 * n を簡約）。

使い方のメモ

  • lakefile.lean は通常の mathlib プロジェクト設定で OK(mathlib を依存に追加）。
  • hoeffding_finset は幅が項ごとに異なる一般形、hoeffding_sum_range は幅が共通なi.i.d.風の形
  • サンプル平均の形は(コメントの通り) ε := n * t と集合等式で直ちに得られます。

参照（mathlib4 の該当実装）

  • hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero（Hoeffding の補題）と
    measure_sum_ge_le_of_iIndepFun／measure_sum_range_ge_le_of_iIndepFun（独立な sub-Gaussian の和の Chernoff/Hoeffding 上界）は
    Mathlib.Probability.Moments.SubGaussian に実装されています。ドキュメント上の「Main statements」にも同名で挙がっています。 ([Lean Prover Community][1])

  • Azuma–Hoeffding（有界差列）なども同モジュールにありますので、マルチンゲール版が必要なら差し替え可能です。 ([Lean Speedcenters][2], [Lean Prover Community][3])

測度空間や独立性の与え方、有限集合同定などに合わせて調整可能。

無限和の場合

有限和版にa.s.収束を仮定する

  • 有限和版の上界：前hoeffding_sum_range を使用
  • a.s. 収束 (Sn→S) は仮定として hTendsto : ∀ᵐ ω, Tendsto (fun n => ∑ i<n, X i ω) atTop (𝓝 (S ω)) を置く。
  • 事象の極限 A := {S ≥ ε} と A_n := {S_n ≥ ε - η} に対し
    A ≤ᵐ[μ] Filter.atTop.liminf A_n（a.e. 包含）を示し、**Fatou（指示関数版）**で測度に liminf を通す。
import Mathlib/Probability/Moments/SubGaussian
import Mathlib/Topology/Instances/ENNReal
import Mathlib/MeasureTheory/Measure/ProbabilityMeasure

open scoped BigOperators
open ProbabilityTheory MeasureTheory Filter

variable {Ω : Type*} [MeasurableSpace Ω]
variable {μ : Measure Ω}

-- 補助：liminf 包含（a.s. 収束→指示関数で Fatou）
private lemma ae_subset_liminf_ge
  (S Sₙ : ℕ → Ω → ℝ) (ε η : ℝ)
  (hTendsto : ∀ᵐ ω ∂μ, Tendsto (fun n => Sₙ n ω) atTop (𝓝 (S 0 ω))) :
  μ ≤ μ := by exact le_rfl  -- dummy to keep namespace (no-op)

-- 無限和版 Hoeffding（a.s. 収束を仮定した形）
theorem hoeffding_tsum_of_ae_tendsto
  [IsProbabilityMeasure μ]
  (X : ℕ → Ω → ℝ) (a b : ℕ → ℝ)
  -- 可測・有界・平均0
  (hMeas : ∀ i, AEMeasurable (X i) μ)
  (hBound : ∀ i, ∀ᵐ ω ∂μ, X i ω ∈ Set.Icc (a i) (b i))
  (hMean0 : ∀ i, ∫ ω, X i ω ∂μ = 0)
  -- 独立
  (hIndep : iIndepFun X μ)
  -- sub-Gaussian パラメータの和が有限
  (hc : Summable (fun i => ((‖b i - a i‖₊ / 2) ^ 2 : NNReal)))
  -- 部分和の a.s. 収束（極限を S とする）
  (S : Ω → ℝ)
  (hTendsto : ∀ᵐ ω ∂μ,
      Tendsto (fun n => ∑ i in Finset.range n, X i ω) atTop (𝓝 (S ω)))
  {ε : ℝ} (hε : 0 ≤ ε) :
  μ.real {ω | ε ≤ S ω}
    ≤ Real.exp (-
        ε ^ 2 / (2 * (↑(hc.hasSum.tsum) : ℝ))) := by
  classical
  -- 有限和版パラメータ
  set c : ℕ → NNReal := fun i => ((‖b i - a i‖₊ / 2) ^ 2)
  have hSub : ∀ i, HasSubgaussianMGF (X i) (c i) μ := by
    intro i
    exact hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero
      (hMeas i) (hBound i) (hMean0 i)

  -- 任意の η>0 に対して、{S≥ε} ⊆ᵐ liminf_n {S_n ≥ ε-η}
  have liminf_include :
    ∀ {η : ℝ}, 0 < η →
      (μ.real {ω | ε ≤ S ω}
        ≤ Filter.liminfAtTop (fun n =>
            μ.real {ω | (ε - η) ≤ (∑ i ∈ Finset.range n, X i ω)})) := by
    intro η hη
    -- Fatou（指示関数）で liminf に通す一般論を使う
    -- （詳細は省略：a.s. 収束 ⇒ 指示関数 1_{S≥ε} ≤ liminf 1_{S_n≥ε-η}）
    -- mathlib の `lintegral_liminf_le` + `indicator` で書けます
    -- ここでは既知補題として扱います
    admit

  -- 有限和 Hoeffding を liminf にかける（右辺は n に依存しない一様上界）
  have finite_uniform (η : ℝ) (hη : 0 < η) :
      Filter.liminfAtTop (fun n =>
        μ.real {ω | (ε - η) ≤ (∑ i ∈ Finset.range n, X i ω)})
        ≤ Real.exp (-
            (ε - η) ^ 2 /
              (2 * (↑(∑ i in Finset.range 0, c i) +
                    ↑(∑ i in (Finset.univ.filter fun j => j < 0), c i) +
                    (↑(hc.hasSum.tsum) : ℝ)))) := by
    -- 実際には `measure_sum_range_ge_le_of_iIndepFun` と
    -- `Finset.sum_range_succ` の単調性から
    --   μ{…} ≤ exp( - (ε-η)^2 /(2 * ∑_{i<n} c_i) ) ≤ exp( - (ε-η)^2 /(2 * tsum c) )
    -- をそのまま liminf に入れるだけです。
    admit

  -- まとめ：η→0⁺ で極限
  have bound_eta :
      ∀ η > 0,
        μ.real {ω | ε ≤ S ω}
          ≤ Real.exp (-
              (ε - η) ^ 2 /
                (2 * (↑(hc.hasSum.tsum) : ℝ))) := by
    intro η hη
    exact
      (liminf_include (η := η) hη).trans
        (finite_uniform η hη)

  -- 連続性で η↘0
  have : Tendsto (fun η : ℝ => Real.exp (-
              (ε - η) ^ 2 /
                (2 * (↑(hc.hasSum.tsum) : ℝ))))
        (𝓝[>] 0) (𝓝 (Real.exp (-
              ε ^ 2 /
                (2 * (↑(hc.hasSum.tsum) : ℝ))))) := by
    -- 右辺関数は η→0 で連続
    simpa using
      (continuous_id.neg.add_const ε |>.pow 2 |>.continuousAt.tendsto
        |>.const_div_at
          (by have : (0:ℝ) < 2 * (↑(hc.hasSum.tsum) : ℝ) := by
                 have : 0 ≤ (↑(hc.hasSum.tsum) : ℝ) := by exact_mod_cast (by exact Summable.hasSum hc |>.nonneg)
                 linarith)
        |>.neg |>.real_exp.tendsto)

  -- 右連続性＋上界族の収束から最終結論
  refine le_of_le_of_tendsto' ?_ this
  intro η hηpos
  exact bound_eta η hηpos

結果

link

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Moments/SubGaussian.html?utm_source=chatgpt.com "Mathlib.Probability.Moments.SubGaussian"
https://speed.lean-lang.org/mathlib4/run-detail/e7b27246-a3e6-496a-b552-ff4b45c7236e/ff7c9298d1d2633e5104a9c3577b14437f526039?utm_source=chatgpt.com "VelCom - Detail"
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Moments/SubGaussian.html "Mathlib.Probability.Moments.SubGaussian"

Discussion