`BookProof.ChapterSequentialBayes.sequential_eq_batch` {prior ℓ₁ ℓ₂ : X → ℝ} (h1 : 0 < totEvidence prior ℓ₁) (h2 : 0 < totEvidence prior (fun x => ℓ₁ x * ℓ₂ x)) :...

Proved

BookProof.ChapterSequentialBayes.sequential_eq_batch

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSequentialBayes.

BookProof.ChapterSequentialBayes.sequential_eq_batch {prior ℓ₁ ℓ₂ : X → ℝ} (h1 : 0 < totEvidence prior ℓ₁) (h2 : 0 < totEvidence prior (fun x => ℓ₁ x * ℓ₂ x)) : bayesUpdate (bayesUpdate prior ℓ₁) ℓ₂ = bayesUpdate prior (fun x => ℓ₁ x * ℓ₂ x)

Formalization note: Lean 4 identifier BookProof.ChapterSequentialBayes.sequential_eq_batch.

Preamble

-- Generated from ChapterSequentialBayes.lean — theorem BookProof.ChapterSequentialBayes.sequential_eq_batch
import Mathlib
import Definitions.Def_ChapterSequentialBayes
open BookProof.ChapterSequentialBayes


open scoped BigOperators


variable {X : Type*} [Fintype X]

Formal statement

theorem BookProof.ChapterSequentialBayes.sequential_eq_batch {prior ℓ₁ ℓ₂ : X → ℝ}
    (h1 : 0 < totEvidence prior ℓ₁)
    (h2 : 0 < totEvidence prior (fun x => ℓ₁ x * ℓ₂ x)) :
    bayesUpdate (bayesUpdate prior ℓ₁) ℓ₂ = bayesUpdate prior (fun x => ℓ₁ x * ℓ₂ x) := by sorry

View graph