`BookProof.ChapterFiniteBayesHierarchy.nestedMarginal_eq_terminalMarginal` (ks : List (S → S → ℝ)) (likelihood : S → ℝ) : nestedMarginal ks likelihood = terminalMarginal (collapseK

Proved

BookProof.ChapterFiniteBayesHierarchy.nestedMarginal_eq_terminalMarginal

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterFiniteBayesHierarchy.

BookProof.ChapterFiniteBayesHierarchy.nestedMarginal_eq_terminalMarginal (ks : List (S → S → ℝ)) (likelihood : S → ℝ) : nestedMarginal ks likelihood = terminalMarginal (collapseKernels ks) likelihood

Formalization note: Lean 4 identifier BookProof.ChapterFiniteBayesHierarchy.nestedMarginal_eq_terminalMarginal.

Preamble

-- Generated from ChapterFiniteBayesHierarchy.lean — theorem BookProof.ChapterFiniteBayesHierarchy.nestedMarginal_eq_terminalMarginal
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.nestedMarginal_eq_terminalMarginal (ks : List (S → S → ℝ))
    (likelihood : S → ℝ) :
    nestedMarginal ks likelihood =
      terminalMarginal (collapseKernels ks) likelihood := by sorry

View graph