theorem other other

`iterFilter_cons`

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

formal statement (Lean)

  56theorem iterFilter_cons (L : Likelihood ι Obs) (o : Obs) (os : List Obs) (p : ProbDist ι) :
  57    iterFilter L (o :: os) p = iterFilter L os (bayesStep p L o) := rfl

proof body

depends on (7)

Lean names referenced from this declaration's body.

ProbDist in IndisputableMonolith.Information.ShannonEntropy decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
bayesStep in IndisputableMonolith.Statistics.BayesianFilteringFromVFE decl_use
iterFilter in IndisputableMonolith.Statistics.BayesianFilteringFromVFE decl_use
Likelihood in IndisputableMonolith.Statistics.BayesianFilteringFromVFE decl_use
ProbDist in IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL decl_use