`BookProof.ChapterDeepLearningMAP.exp_logObjective` (prior : Model → ℝ) (likelihood : Model → Data → ℝ) (d : Data) (hprior : ∀ m, 0 < prior m) (hlike : ∀ m, 0 < likelihood m d) (m

Proved

BookProof.ChapterDeepLearningMAP.exp_logObjective

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDeepLearningMAP.

BookProof.ChapterDeepLearningMAP.exp_logObjective (prior : Model → ℝ) (likelihood : Model → Data → ℝ) (d : Data) (hprior : ∀ m, 0 < prior m) (hlike : ∀ m, 0 < likelihood m d) (m : Model) : Real.exp (logObjective prior likelihood d m) = posteriorWeight prior likelihood d m

Formalization note: Lean 4 identifier BookProof.ChapterDeepLearningMAP.exp_logObjective.

Preamble

-- Generated from ChapterDeepLearningMAP.lean — theorem BookProof.ChapterDeepLearningMAP.exp_logObjective
import Mathlib
import Definitions.Def_ChapterDeepLearningMAP
open BookProof.ChapterDeepLearningMAP



variable {Model Data : Type*}

Formal statement

theorem BookProof.ChapterDeepLearningMAP.exp_logObjective (prior : Model → ℝ) (likelihood : Model → Data → ℝ)
    (d : Data) (hprior : ∀ m, 0 < prior m)
    (hlike : ∀ m, 0 < likelihood m d) (m : Model) :
    Real.exp (logObjective prior likelihood d m) =
      posteriorWeight prior likelihood d m := by sorry

View graph