增加数据总能减少后验方差吗？Does additional data always reduce posterior variance?

今天午餐时的一次讨论提到了一个事实：增加数据并不总能缩小置信区间的范围。这篇文章将从贝叶斯的角度来探讨这个问题。

通常来说，新信息会减少你对所估计事物的不确定性。随着收集到的数据越来越多，后验分布会变得更加集中。

这是“通常”情况下的现象，但这在每次获得新数据时都必然发生吗？可以想象，如果你得到了令人惊讶的数据，即在当前先验条件下极不可能发生的数据，后验的不确定性反而可能会增加。

二项-贝塔模型

为了证明情况确实如此，假设某个二元试验成功的概率为参数 θ，并且 θ 具有一个 Beta 先验。你可以把这个先验想象成在进行了若干次先前观察后得到的后验。一个新的观察结果会增加 θ 的后验方差吗？如果是，在什么条件下？

Beta(a, b) 随机变量的方差为

ab / (a + b)²(a + b + 1)。

在观察到一次成功的试验后，θ 的后验分布为 beta(a + 1, b)。我们可以计算后验方差与先验方差的比值，并探讨在什么情况下（如果有的话）该比值会大于 1。

如果 2a ≥ b，后验方差将严格小于先验方差。这意味着如果先验的平均失败赔率不超过 2:1，观察到一次成功将会减小方差。（观察到一次失败也是如此。）但是对于任何给定的 b 值，你总能找到一个足够小的 a 值，使得观察到一次成功反而会增加方差。

正态-正态模型

观测值是否会增加后验方差取决于数据模型。如果你的数据具有方差已知的正态似然函数，并且均值 θ 具有正态先验，那么后验方差总是小于先验方差，并且无论观测值 x 是多少，它减少的量都是相同的。如果 x 在先验条件下极不可能发生，那么它会将后验均值拉向自己，其力度大于与先验更一致的观测值，但后验方差的变化量是相同的。

贝塔定理的证明

以下是使用 Lean 4 对上述命题（即如果 2a ≥ b，后验方差将严格小于先验方差）的证明。

import Mathlib

set_option linter.style.header false

noncomputable def f (a b : ℝ) : ℝ := a * b / ((a + b) ^ 2 * (a + b + 1))

theorem f_ratio_lt_one' (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : b ≤ 2 * a) :
    f (a + 1) b / f a b < 1 := by
  have hs : 0 < a + b := by linarith
  have h2ab : 0 ≤ 2 * a - b := by linarith
  have hprod : 0 ≤ (a + b) * (2 * a - b) := mul_nonneg hs.le h2ab
  -- key polynomial inequality (∗)
  have key : (a + 1) * (a + b) ^ 2 < a * ((a + b + 1) * (a + b + 2)) := by
    nlinarith [hprod, ha]
  -- nonzero facts needed to clear denominators
  have ha' : a ≠ 0 := ne_of_gt ha
  have hb' : b ≠ 0 := ne_of_gt hb
  have hs' : a + b ≠ 0 := ne_of_gt hs
  have hs1' : a + b + 1 ≠ 0 := by positivity
  have hs2' : a + b + 2 ≠ 0 := by positivity
  have ha1' : a + 1 ≠ 0 := by positivity
  -- express the ratio as a single closed-form fraction
  have hratio : f (a + 1) b / f a b
      = ((a + 1) * (a + b) ^ 2) / (a * ((a + b + 1) * (a + b + 2))) := by
    unfold f
    have e : a + 1 + b = a + b + 1 := by ring
    rw [e]
    field_simp
    ring
  rw [hratio, div_lt_one (by positivity)]
  exact key