`BookProof.ChapterBayesInference.evidence_nonneg` (hprior : ∀ x, 0 ≤ prior x) (hL : ∀ x y, 0 ≤ L x y) (y : Y) : 0 ≤ evidence prior L y

Initializing...

`BookProof.ChapterBayesInference.evidence_nonneg` (hprior : ∀ x, 0 ≤ prior x) (hL : ∀ x y, 0 ≤ L x y) (y : Y) : 0 ≤ evidence prior L y · Prove2Me