Likelihood
plain-language theorem explainer
The Likelihood structure packages a positive real-valued map from observations to states. It is cited by evidence, bayesStep and BayesianFilteringCert when deriving one-step variational updates. The declaration is a direct structure definition with a positivity field and no further computation.
Claim. Let $ι$ and $Obs$ be types. A likelihood consists of a function $like : Obs → ι → ℝ$ such that $like(o,i) > 0$ for every observation $o$ and state $i$.
background
The module treats discrete Bayesian filtering as one-step minimization of variational free energy. Evidence is defined as the sum over states of prior probability times likelihood value. BayesianFilteringCert then asserts that the normalized update equals the Bayes step. The Likelihood structure supplies the positive observation model required by these constructions.
proof idea
Structure definition. The two fields are introduced directly; no tactics or lemmas are applied.
why it matters
It supplies the observation model for the Bayesian update realized in bayesStep and certified in BayesianFilteringCert. These realize the module claim that a Bayesian update is the one-step VFE minimizer. The positivity field ensures the evidence sum is strictly positive, which is used in downstream weight calculations such as eventWeight_pos.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.