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

Proved

BookProof.ChapterDeepLearningMAP.logObjective_le_iff

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDeepLearningMAP.

BookProof.ChapterDeepLearningMAP.logObjective_le_iff (prior : Model → ℝ) (likelihood : Model → Data → ℝ) (d : Data) (hprior : ∀ m, 0 < prior m) (hlike : ∀ m, 0 < likelihood m d) (a b : Model) : logObjective prior likelihood d a ≤ logObjective prior likelihood d b ↔ posteriorWeight prior likelihood d a ≤ posteriorWeight prior likelihood d b

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

Preamble

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



variable {Model Data : Type*}

Formal statement

theorem BookProof.ChapterDeepLearningMAP.logObjective_le_iff (prior : Model → ℝ)
    (likelihood : Model → Data → ℝ) (d : Data)
    (hprior : ∀ m, 0 < prior m) (hlike : ∀ m, 0 < likelihood m d)
    (a b : Model) :
    logObjective prior likelihood d a ≤ logObjective prior likelihood d b ↔
      posteriorWeight prior likelihood d a ≤ posteriorWeight prior likelihood d b := by sorry

View graph