`BookProof.ChapterObservableExpectation.bayesPosterior_sum_one` {prior : Fin m → ℝ} {L : Fin m → Y → ℝ} (y : Y) (hy : 0 < evidence prior L y) : ∑ x, posterior prior L y x = 1

Initializing...

`BookProof.ChapterObservableExpectation.bayesPosterior_sum_one` {prior : Fin m → ℝ} {L : Fin m → Y → ℝ} (y : Y) (hy : 0 < evidence prior L y) : ∑ x, posterior prior L y x = 1 · Prove2Me