`BookProof.ChapterObservableExpectation.bayes_posterior_expectation_mem_convexHull` (prior : Fin m → ℝ) (L : Fin m → Y → ℝ) (y : Y) (hprior : ∀ x, 0 ≤ prior x) (hL : ∀ x y, 0 ≤ L x

Initializing...

`BookProof.ChapterObservableExpectation.bayes_posterior_expectation_mem_convexHull` (prior : Fin m → ℝ) (L : Fin m → Y → ℝ) (y : Y) (hprior : ∀ x, 0 ≤ prior x) (hL : ∀ x y, 0 ≤ L x · Prove2Me