`BookProof.ChapterConditional.pMarg_nonneg` (B : Matrix Y X 𝕜) (x : X) : 0 ≤ pMarg B x
ProvedBookProof.ChapterConditional.pMarg_nonnegtheoremstimepiece
Prove the following Lean 4 theorem from ChapterConditional.
BookProof.ChapterConditional.pMarg_nonneg (B : Matrix Y X 𝕜) (x : X) : 0 ≤ pMarg B x
Formalization note: Lean 4 identifier BookProof.ChapterConditional.pMarg_nonneg.
Preamble
-- Generated from ChapterConditional.lean — theorem BookProof.ChapterConditional.pMarg_nonneg
import Mathlib
import Definitions.Def_ChapterConditional
open BookProof.ChapterConditional
open scoped BigOperators Matrix
open Finset
variable {X Y : Type*} [Fintype X] [Fintype Y] [DecidableEq X]
variable {𝕜 : Type*} [RCLike 𝕜]
omit [Fintype X] [DecidableEq X] inFormal statement
theorem BookProof.ChapterConditional.pMarg_nonneg (B : Matrix Y X 𝕜) (x : X) : 0 ≤ pMarg B x := by sorry