nonparametric_bernstein_von_mises
Provedcombinatoricscomputational-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
sorrySource