def
definition
evidence
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Statistics.BayesianFilteringFromVFE on GitHub at line 22.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
19 like : Obs → ι → ℝ
20 like_pos : ∀ o i, 0 < like o i
21
22def evidence (prior : ProbDist ι) (L : Likelihood ι Obs) (o : Obs) : ℝ :=
23 ∑ i, prior.prob i * L.like o i
24
25theorem evidence_pos (prior : ProbDist ι) (L : Likelihood ι Obs) (o : Obs) :
26 0 < evidence prior L o := by
27 unfold evidence
28 apply Finset.sum_pos
29 · intro i _
30 exact mul_pos (prior.prob_pos i) (L.like_pos o i)
31 · exact Finset.univ_nonempty
32
33def bayesStep (prior : ProbDist ι) (L : Likelihood ι Obs) (o : Obs) : ProbDist ι :=
34{ prob := fun i => prior.prob i * L.like o i / evidence prior L o
35 prob_pos := by
36 intro i
37 exact div_pos (mul_pos (prior.prob_pos i) (L.like_pos o i)) (evidence_pos prior L o)
38 prob_sum := by
39 unfold evidence
40 rw [← Finset.sum_div]
41 exact div_self (ne_of_gt (evidence_pos prior L o)) }
42
43theorem bayesStep_is_update (prior : ProbDist ι) (L : Likelihood ι Obs) (o : Obs) :
44 ∀ i, (bayesStep prior L o).prob i =
45 prior.prob i * L.like o i / evidence prior L o := by
46 intro i
47 rfl
48
49def iterFilter (L : Likelihood ι Obs) : List Obs → ProbDist ι → ProbDist ι
50 | [], p => p
51 | o :: os, p => iterFilter L os (bayesStep p L o)
52