Posterior odds, Bayes factors, and model-odds update
Definitionfep2_bayesian_model_reductionThe Bayesian-model-reduction comparison layer over the published Free Energy Principle I finite substrate.
For two hypotheses of a finite model family, the posterior odds at evidence with positive predictive mass is the ratio of their exact finite Bayes posteriors,
The Bayes factor is the evidence ratio of the favored against the reference model, and the updated model odds apply one reduction step,
the multiplicative update Bayesian model reduction performs when comparing a reduced model against the model it was reduced from.
Real division is totalized: a zero reference mass yields , not an infinite odds value, so supported comparisons must carry the nonzero-denominator premises explicitly — the same boundary honesty as the FEP-I substrate.
import Definitions.Def_fep_finite_laws
import Mathlib.Tactic
/-!
# Bayesian model reduction (mission substrate)
Mission `Free Energy Principle II` Bayesian-model-reduction substrate,
transcribed from the proved module `FepSketches.learning_theory` of the
fep_lean formalization (Active Inference Institute), reusing the published
`Free Energy Principle I` finite substrate. Model comparison is carried by
explicit real-valued odds: posterior odds between two hypotheses given
positive evidence, the likelihood ratio as a finite Bayes factor, and the
model-odds update `posterior odds = prior odds × Bayes factor` that Bayesian
model reduction applies when evidence factorizes over models.
-/
namespace FreeEnergyPrinciple
open Finset
open scoped BigOperators
/-- Posterior odds between two finite hypotheses at positive evidence. -/
noncomputable def posteriorOdds
{Hypothesis Evidence : Type*} [Fintype Hypothesis] [Fintype Evidence]
(prior : FiniteLaw Hypothesis)
(likelihood : FiniteKernel Hypothesis Evidence)
(evidence : Evidence)
(evidencePositive : 0 < likelihood.predictive prior evidence)
(favored reference : Hypothesis) : ℝ :=
likelihood.posterior prior evidence evidencePositive favored /
likelihood.posterior prior evidence evidencePositive reference
/-- Likelihood ratio used as a finite Bayes factor. -/
noncomputable def bayesFactor (favored reference : ℝ) : ℝ :=
favored / reference
/-- Posterior model odds after one evidence update. -/
noncomputable def updatedModelOdds
(priorOdds favoredEvidence referenceEvidence : ℝ) : ℝ :=
priorOdds * bayesFactor favoredEvidence referenceEvidence
end FreeEnergyPrinciple
Read-back
What the Lean code literally says, in plain math · glm-flash-latest
The file defines three real-valued functions in namespace FreeEnergyPrinciple.
1. posteriorOdds. For finite types Hypothesis and Evidence, given: a prior law on hypotheses (a FiniteLaw from the FEP-I finite substrate), a likelihood kernel from hypotheses to evidence (a FiniteKernel), an evidence point , the hypothesis that the predictive probability of is strictly positive, i.e. , and two hypotheses, (favored) and (reference), it defines
where is the posterior probability of hypothesis given computed by the kernel's posterior operation from the same substrate.
2. bayesFactor. For arbitrary real numbers and , defines . No sign or positivity condition is imposed.
3. updatedModelOdds. For arbitrary reals , , , defines , the literal product of the first argument with the likelihood ratio of the second over the third.
AUDITOR-FLAG: the denominator of posteriorOdds is never assumed positive (only the predictive is); if the reference hypothesis has posterior zero, the quotient is the Lean junk value for division by zero, not an undefined quantity. AUDITOR-FLAG: favored and reference hypotheses are not required to be distinct or comparable. AUDITOR-FLAG: bayesFactor silently returns when its second argument is . AUDITOR-FLAG: updatedModelOdds accepts any three reals; nothing in the definition enforces that its arguments are odds or likelihood ratios — all semantic content lives in the caller.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.