`BookProof.ChapterHierarchicalBayes.jointPrior_sum_one` (outer : A → ℝ) (inner : A → B → ℝ) (hOuter : ∑ a, outer a = 1) (hInner : ∀ a, ∑ b, inner a b = 1) : ∑ a, ∑ b, jointPrior ou

Proved

BookProof.ChapterHierarchicalBayes.jointPrior_sum_one

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterHierarchicalBayes.

BookProof.ChapterHierarchicalBayes.jointPrior_sum_one (outer : A → ℝ) (inner : A → B → ℝ) (hOuter : ∑ a, outer a = 1) (hInner : ∀ a, ∑ b, inner a b = 1) : ∑ a, ∑ b, jointPrior outer inner a b = 1

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

Preamble

-- Generated from ChapterHierarchicalBayes.lean — theorem BookProof.ChapterHierarchicalBayes.jointPrior_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.jointPrior_sum_one (outer : A → ℝ) (inner : A → B → ℝ)
    (hOuter : ∑ a, outer a = 1) (hInner : ∀ a, ∑ b, inner a b = 1) :
    ∑ a, ∑ b, jointPrior outer inner a b = 1 := by sorry

View graph