`BookProof.ChapterUniformPriorPosterior.exists_likelihood_uniform_prior_posterior` (q : Hyp → ℝ) (hq_nonneg : ∀ x, 0 ≤ q x) (hq_sum : ∑ x, q x = 1) (c : ℝ) (hc : 0 < c) : ∃ L : Hyp

Proved

BookProof.ChapterUniformPriorPosterior.exists_likelihood_uniform_prior_posterior

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterUniformPriorPosterior.

BookProof.ChapterUniformPriorPosterior.exists_likelihood_uniform_prior_posterior (q : Hyp → ℝ) (hq_nonneg : ∀ x, 0 ≤ q x) (hq_sum : ∑ x, q x = 1) (c : ℝ) (hc : 0 < c) : ∃ L : Hyp → Bool → ℝ, (∀ x observed, 0 ≤ L x observed) ∧ (∀ x, ∑ observed, L x observed = 1) ∧ (∀ x, BookProof.ChapterBayesInference.posterior (fun _ : Hyp => c) L true x = q x)

Formalization note: Lean 4 identifier BookProof.ChapterUniformPriorPosterior.exists_likelihood_uniform_prior_posterior.

Preamble

-- Generated from ChapterUniformPriorPosterior.lean — theorem BookProof.ChapterUniformPriorPosterior.exists_likelihood_uniform_prior_posterior
import Mathlib
import Definitions.Def_ChapterUniformPriorPosterior
import Definitions.Def_ChapterBayesInference
open BookProof.ChapterBayesInference
open BookProof.ChapterUniformPriorPosterior


open scoped BigOperators


variable {Hyp : Type*} [Fintype Hyp] [DecidableEq Hyp]

Formal statement

theorem BookProof.ChapterUniformPriorPosterior.exists_likelihood_uniform_prior_posterior (q : Hyp → ℝ)
    (hq_nonneg : ∀ x, 0 ≤ q x) (hq_sum : ∑ x, q x = 1)
    (c : ℝ) (hc : 0 < c) :
    ∃ L : Hyp → Bool → ℝ,
      (∀ x observed, 0 ≤ L x observed) ∧
      (∀ x, ∑ observed, L x observed = 1) ∧
      (∀ x, BookProof.ChapterBayesInference.posterior (fun _ : Hyp => c)
        L true x = q x) := by sorry

View graph