`BookProof.ChapterSequentialBayes.bayesUpdate_evidence` {prior ℓ₁ ℓ₂ : X → ℝ} : (∑ x, bayesUpdate prior ℓ₁ x * ℓ₂ x) = (∑ x, prior x * (ℓ₁ x * ℓ₂ x)) / (∑ x,...
ProvedBookProof.ChapterSequentialBayes.bayesUpdate_evidencetheoremstimepiece
Prove the following Lean 4 theorem from ChapterSequentialBayes.
BookProof.ChapterSequentialBayes.bayesUpdate_evidence {prior ℓ₁ ℓ₂ : X → ℝ} : (∑ x, bayesUpdate prior ℓ₁ x * ℓ₂ x) = (∑ x, prior x * (ℓ₁ x * ℓ₂ x)) / (∑ x, prior x * ℓ₁ x)
Formalization note: Lean 4 identifier BookProof.ChapterSequentialBayes.bayesUpdate_evidence.
Preamble
-- Generated from ChapterSequentialBayes.lean — theorem BookProof.ChapterSequentialBayes.bayesUpdate_evidence
import Mathlib
import Definitions.Def_ChapterSequentialBayes
open BookProof.ChapterSequentialBayes
open scoped BigOperators
variable {X : Type*} [Fintype X]Formal statement
theorem BookProof.ChapterSequentialBayes.bayesUpdate_evidence {prior ℓ₁ ℓ₂ : X → ℝ} :
(∑ x, bayesUpdate prior ℓ₁ x * ℓ₂ x)
= (∑ x, prior x * (ℓ₁ x * ℓ₂ x)) / (∑ x, prior x * ℓ₁ x) := by sorry