`BookProof.ChapterFiniteBayesHierarchy.collapseKernels_nonnegative` (ks : List (S → S → ℝ)) (hks : ∀ k ∈ ks, IsNonnegativeKernel k) : IsNonnegativeKernel (collapseKernels ks)
ProvedBookProof.ChapterFiniteBayesHierarchy.collapseKernels_nonnegativetheoremstimepiece
Prove the following Lean 4 theorem from ChapterFiniteBayesHierarchy.
BookProof.ChapterFiniteBayesHierarchy.collapseKernels_nonnegative (ks : List (S → S → ℝ)) (hks : ∀ k ∈ ks, IsNonnegativeKernel k) : IsNonnegativeKernel (collapseKernels ks)
Formalization note: Lean 4 identifier BookProof.ChapterFiniteBayesHierarchy.collapseKernels_nonnegative.
Preamble
-- Generated from ChapterFiniteBayesHierarchy.lean — theorem BookProof.ChapterFiniteBayesHierarchy.collapseKernels_nonnegative
import Mathlib
import Definitions.Def_ChapterFiniteBayesHierarchy
import Definitions.Def_ChapterHierarchicalBayesComposition
open BookProof.ChapterHierarchicalBayesComposition
open BookProof.ChapterFiniteBayesHierarchy
open scoped BigOperators
open BookProof.ChapterHierarchicalBayesComposition
variable {S : Type*} [Fintype S] [DecidableEq S]Formal statement
theorem BookProof.ChapterFiniteBayesHierarchy.collapseKernels_nonnegative (ks : List (S → S → ℝ))
(hks : ∀ k ∈ ks, IsNonnegativeKernel k) :
IsNonnegativeKernel (collapseKernels ks) := by sorry