Bayesian Inference and Learners

BayesianInference bundles prior, likelihood, and posterior computation. BayesianLearner extends BatchLearner with Bayesian inference machinery. GibbsPosterior adds temperature for PAC-Bayes optimization.

structure BayesianInference (X : Type u) (Y : Type v) [MeasurableSpace X] : Type (max u v)

Bayesian inference: bundles prior, likelihood model, and posterior computation.

• prior : Concept X Y → ℝ

  Prior distribution over hypotheses

• likelihood : Concept X Y → X × Y → ℝ

  Likelihood: probability of data given hypothesis

• posterior (h : Concept X Y) (data : List (X × Y)) : ℝ

  Posterior: prior(h) × ∏ likelihood(h, dᵢ). Unnormalized; the normalization constant Z = Σ_h' prior(h') × ∏ likelihood(h', dᵢ) is omitted because computing it requires summing over all hypotheses (which may be uncountable). Downstream definitions that need a proper probability must normalize explicitly. This is the standard "unnormalized posterior" used in computational Bayesian inference.

structure BayesianLearner (X : Type u) (Y : Type v) [MeasurableSpace X] : Type (max u v)

A Bayesian learner carries a prior and updates via Bayes' rule.

• hypotheses : HypothesisSpace X Y

  The hypothesis space

• inference : BayesianInference X Y

  Bayesian inference engine

• learnMAP {m : ℕ} : (Fin m → X × Y) → Concept X Y

  MAP learner: output the maximum a posteriori hypothesis

• output_in_H {m : ℕ} (S : Fin m → X × Y) : self.learnMAP S ∈ self.hypotheses

  Output is in hypothesis space

structure GibbsPosterior (X : Type u) (Y : Type v) [MeasurableSpace X] : Type (max u v)

Gibbs posterior: a Bayesian learner that uses a tempered posterior (PAC-Bayes bound optimization).

• base : BayesianLearner X Y

  Base Bayesian learner

• lambda : ℝ

  Temperature parameter (inverse)

• lambda_pos : 0 < self.lambda

  Temperature is positive