`BookProof.ChapterUniformPrior.uniform_prior_isMAP_iff_isMLE` [Fintype Hyp] (likelihood : Hyp → Data → ℝ) (d : Data) (c : ℝ) (hc : 0 < c) (hevidence : 0 < BookProof.ChapterBayesInf

Proved

BookProof.ChapterUniformPrior.uniform_prior_isMAP_iff_isMLE

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterUniformPrior.

BookProof.ChapterUniformPrior.uniform_prior_isMAP_iff_isMLE [Fintype Hyp] (likelihood : Hyp → Data → ℝ) (d : Data) (c : ℝ) (hc : 0 < c) (hevidence : 0 < BookProof.ChapterBayesInference.evidence (fun _ : Hyp => c) likelihood d) (best : Hyp) : (∀ m, BookProof.ChapterBayesInference.posterior (fun _ : Hyp => c) likelihood d m ≤ BookProof.ChapterBayesInference.posterior (fun _ : Hyp => c) likelihood d best) ↔ ∀ m, likelihood m d ≤ likelihood best d

Formalization note: Lean 4 identifier BookProof.ChapterUniformPrior.uniform_prior_isMAP_iff_isMLE.

Preamble

-- Generated from ChapterUniformPrior.lean — theorem BookProof.ChapterUniformPrior.uniform_prior_isMAP_iff_isMLE
import Mathlib
import Definitions.Def_ChapterUniformPrior
import Definitions.Def_ChapterBayesInference
open BookProof.ChapterBayesInference
open BookProof.ChapterUniformPrior


open scoped BigOperators


variable {Hyp Data : Type*}

Formal statement

theorem BookProof.ChapterUniformPrior.uniform_prior_isMAP_iff_isMLE [Fintype Hyp]
    (likelihood : Hyp → Data → ℝ) (d : Data) (c : ℝ)
    (hc : 0 < c)
    (hevidence : 0 < BookProof.ChapterBayesInference.evidence (fun _ : Hyp => c) likelihood d)
    (best : Hyp) :
    (∀ m, BookProof.ChapterBayesInference.posterior (fun _ : Hyp => c) likelihood d m ≤
        BookProof.ChapterBayesInference.posterior (fun _ : Hyp => c) likelihood d best) ↔
      ∀ m, likelihood m d ≤ likelihood best d := by sorry

View graph