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

Proved

BookProof.ChapterHierarchicalBayes.flatPosterior_sum_one

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterHierarchicalBayes.

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

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

Preamble

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

View graph