`BookProof.ChapterHierarchicalBayes.evidence_eq_marginal` (outer : A → ℝ) (inner : A → B → ℝ) (likelihood : A → B → ℝ) : hierEvidence outer inner likelihood = ∑ a, outer a * margin

Proved

BookProof.ChapterHierarchicalBayes.evidence_eq_marginal

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterHierarchicalBayes.

BookProof.ChapterHierarchicalBayes.evidence_eq_marginal (outer : A → ℝ) (inner : A → B → ℝ) (likelihood : A → B → ℝ) : hierEvidence outer inner likelihood = ∑ a, outer a * marginalLikelihood inner likelihood a

Formalization note: Lean 4 identifier BookProof.ChapterHierarchicalBayes.evidence_eq_marginal.

Preamble

-- Generated from ChapterHierarchicalBayes.lean — theorem BookProof.ChapterHierarchicalBayes.evidence_eq_marginal
import Mathlib
import Definitions.Def_ChapterHierarchicalBayes
open BookProof.ChapterHierarchicalBayes


open scoped BigOperators


variable {A B : Type*} [Fintype A] [Fintype B]

Formal statement

theorem BookProof.ChapterHierarchicalBayes.evidence_eq_marginal (outer : A → ℝ) (inner : A → B → ℝ)
    (likelihood : A → B → ℝ) :
    hierEvidence outer inner likelihood =
      ∑ a, outer a * marginalLikelihood inner likelihood a := by sorry

View graph