`BookProof.ChapterHierarchicalBayes.jointPrior_nonneg` (outer : A → ℝ) (inner : A → B → ℝ) (hOuter : ∀ a, 0 ≤ outer a) (hInner : ∀ a b, 0 ≤ inner a b) : ∀ a b, 0 ≤...

Proved

BookProof.ChapterHierarchicalBayes.jointPrior_nonneg

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterHierarchicalBayes.

BookProof.ChapterHierarchicalBayes.jointPrior_nonneg (outer : A → ℝ) (inner : A → B → ℝ) (hOuter : ∀ a, 0 ≤ outer a) (hInner : ∀ a b, 0 ≤ inner a b) : ∀ a b, 0 ≤ jointPrior outer inner a b

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

Preamble

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

View graph