iterFilter
plain-language theorem explainer
iterFilter recursively applies the single-step Bayesian update to a list of observations, yielding the posterior after sequential filtering. Researchers deriving multi-step posteriors from variational free energy would reference this when extending the one-step minimizer to finite sequences. The definition proceeds by direct recursion on the observation list with base case returning the prior unchanged.
Claim. Define the iterative filter recursively by $iterFilter(L, [], p) := p$ and $iterFilter(L, o :: os, p) := iterFilter(L, os, bayesStep(p, L, o))$, where $L$ is a likelihood structure providing positive densities $like(o, i)$ for each observation $o$ and state $i$, $p$ is a probability distribution over states, and $bayesStep$ performs the normalized update $p(i) · like(o,i) / evidence$.
background
Bayesian filtering here operates on discrete state spaces. A Likelihood structure consists of a function assigning positive real values to each observation-state pair together with a positivity proof. A ProbDist is a function from states to positive reals summing to one, as defined in the Shannon entropy module and the variational free energy module. The module establishes that a single Bayesian update minimizes the variational free energy derived from the recognition composition law. The iterFilter definition extends this one-step minimizer to arbitrary finite lists of observations by recursion. Upstream, bayesStep is defined using the evidence normalizer to produce a valid posterior distribution.
proof idea
The definition is given by pattern matching on the observation list: the empty list returns the input distribution unchanged, while a non-empty list applies bayesStep to the head observation and recurses on the tail. No lemmas are invoked; it is a direct structural recursion.
why it matters
This definition supplies the multi-step extension of the one-step VFE minimizer, feeding directly into the cons and nil lemmas that establish its recursive properties. It realizes the discrete filtering surface described in the module, connecting the recognition composition law through variational free energy to sequential Bayesian inference. No open questions are addressed here; it closes the basic recursive construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.