pith. machine review for the scientific record. sign in
def definition def or abbrev

bayesStep

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

formal statement (Lean)

  33def bayesStep (prior : ProbDist ι) (L : Likelihood ι Obs) (o : Obs) : ProbDist ι :=

proof body

Definition body.

  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

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.