`BookProof.ChapterHierarchicalBayes.outerPosterior_sum_one` (outer : A → ℝ) (inner : A → B → ℝ) (likelihood : A → B → ℝ) (hEvidence : 0 < hierEvidence outer inner likelihood) : ∑ a

Proved

BookProof.ChapterHierarchicalBayes.outerPosterior_sum_one

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterHierarchicalBayes.

BookProof.ChapterHierarchicalBayes.outerPosterior_sum_one (outer : A → ℝ) (inner : A → B → ℝ) (likelihood : A → B → ℝ) (hEvidence : 0 < hierEvidence outer inner likelihood) : ∑ a, outerPosterior outer inner likelihood a = 1

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

Preamble

-- Generated from ChapterHierarchicalBayes.lean — theorem BookProof.ChapterHierarchicalBayes.outerPosterior_sum_one
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.outerPosterior_sum_one (outer : A → ℝ) (inner : A → B → ℝ)
    (likelihood : A → B → ℝ)
    (hEvidence : 0 < hierEvidence outer inner likelihood) :
    ∑ a, outerPosterior outer inner likelihood a = 1 := by sorry

View graph