module module

`IndisputableMonolith.Statistics.BayesianFilteringFromVFE`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL module_import

declarations in this module (10)

structure Likelihood L18
def evidence L22
theorem evidence_pos L25
def bayesStep L33
theorem bayesStep_is_update L43
def iterFilter L49
theorem iterFilter_nil L53
theorem iterFilter_cons L56
structure BayesianFilteringCert L59
theorem bayesianFilteringCert_holds L66