`BookProof.ChapterBayesInference.posterior_eq_born_conditional` (hprior : ∀ x, 0 ≤ prior x) (hL : ∀ x y, 0 ≤ L x y) (y : Y) (x : X) : posterior prior L y x = (Real.sqrt (joint prio

Initializing...

`BookProof.ChapterBayesInference.posterior_eq_born_conditional` (hprior : ∀ x, 0 ≤ prior x) (hL : ∀ x y, 0 ≤ L x y) (y : Y) (x : X) : posterior prior L y x = (Real.sqrt (joint prio · Prove2Me