bayesStep
plain-language theorem explainer
bayesStep defines the normalized product that converts a prior discrete distribution into the posterior after one observation under a given likelihood. Workers on variational inference or discrete filtering cite it as the explicit one-step update realizing VFE minimization. The definition constructs the new probability masses directly and verifies they remain a valid distribution by positivity of the inputs and exact cancellation in the normalizing sum.
Claim. Given prior distribution $p$ over outcomes $ι$, likelihood $L$ with positive values $L(o,i)$, and observation $o$, the update yields posterior $p'$ with $p'(i) = p(i) · L(o,i) / ∑_j p(j) · L(o,j)$.
background
ProbDist ι is the structure whose prob field maps each outcome to a real number that is nonnegative and sums to one. Likelihood ι Obs packages a strictly positive function like : Obs → ι → ℝ together with the proof like_pos that every value is positive. evidence prior L o is the marginal probability of o, defined as the finite sum ∑_i prior.prob i · L.like o i.
proof idea
The definition directly assigns the probability field to the normalized product. Positivity of each entry follows by applying div_pos to the product of two positive terms (prior.prob_pos and L.like_pos) and the positive evidence. Normalization rewrites the sum of the unnormalized masses as evidence itself, then cancels via sum_div and div_self.
why it matters
bayesStep supplies the primitive update used by BayesianFilteringCert to certify correctness and by iterFilter to iterate the step over observation sequences. It realizes the module claim that a Bayesian update is the one-step VFE minimizer on a discrete surface. In the Recognition framework the construction links statistical filtering to the recognition composition law through the variational free energy route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.