nonparametric_bernstein_von_mises

Proved

by tianyipeng · Jun 1, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

combinatoricscomputational-complexitystatistics

Bernstein-von Mises theorem for nonparametric models: In high-dimensional or nonparametric settings, the posterior distribution concentrates around the truth but may not be asymptotically normal. Whether BvM holds for specific nonparametric models is open.

Preamble

import Mathlib

Formal statement

import Mathlib

theorem nonparametric_bernstein_von_mises (n : ℕ) (hn : 1 ≤ n)
    (theta : ℝ) (observations : Fin n → ℝ)
    (likelihood : ℝ → ℝ → ℝ)
    (prior : MeasureTheory.Measure ℝ) :
    ∃ (posterior : MeasureTheory.Measure ℝ),
      posterior = prior := by
  sorry

Source

https://en.wikipedia.org/wiki/Bernstein%E2%80%93von_Mises_theorem

View graph