Utility–loss duality for finite decision problems

The bridge between [vR03a]'s utility scale (DecisionProblem, questionUtility over ℝ) and mathlib's loss scale (ProbabilityTheory.bayesRisk over ℝ≥0∞): for a bound C above every utility, the Bayes risk of the partition experiment under the regret loss C − U equals C minus the partition's decision value (bayesRisk_deterministic_regretLoss). Through it, [vR03a]'s §4.1 Fact becomes a biconditional theorem about the Blackwell order:

• forward (questionUtility_comp_le): coarsening the classifier cannot raise question utility — the partition instance of the data-processing inequality bayesRisk_deterministic_le_deterministic_comp;
• converse (factorsThrough_of_forall_questionUtility_le): a partition whose question utility is dominated in every decision problem factors through the dominating one — the Blackwell–Sherman–Stein converse (isGarblingOf_of_blackwellDominates) plus the deterministic factoring characterization (Kernel.deterministic_isGarblingOf_deterministic_iff).

noncomputable def Core.DecisionTheory.DecisionProblem.priorMeasure {W : Type u_1} {A : Type u_2} [Fintype W] [MeasurableSpace W] (dp : DecisionProblem ℝ W A) : MeasureTheory.Measure W

The prior of a decision problem as a measure: the weighted sum of Dirac masses ∑ w, ofReal (prior w) • δ_w.

Equations

• dp.priorMeasure = ∑ w : W, ENNReal.ofReal (dp.prior w) • MeasureTheory.Measure.dirac w

@[simp]

theorem Core.DecisionTheory.DecisionProblem.priorMeasure_singleton {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [MeasurableSpace W] [MeasurableSingletonClass W] (dp : DecisionProblem ℝ W A) (w : W) : dp.priorMeasure {w} = ENNReal.ofReal (dp.prior w)

instance Core.DecisionTheory.DecisionProblem.instIsFiniteMeasurePriorMeasure {W : Type u_1} {A : Type u_2} [Fintype W] [MeasurableSpace W] (dp : DecisionProblem ℝ W A) : MeasureTheory.IsFiniteMeasure dp.priorMeasure

theorem Core.DecisionTheory.DecisionProblem.isProbabilityMeasure_priorMeasure {W : Type u_1} {A : Type u_2} [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] (dp : DecisionProblem ℝ W A) (hprior : ∀ (w : W), 0 ≤ dp.prior w) (hsum : ∑ w : W, dp.prior w = 1) : MeasureTheory.IsProbabilityMeasure dp.priorMeasure

noncomputable def Core.DecisionTheory.DecisionProblem.regretLoss {W : Type u_1} {A : Type u_2} (dp : DecisionProblem ℝ W A) (C : ℝ) : W → A → ENNReal

The regret loss at bound C: ℓ(w, a) = C − U(w, a), clamped into ℝ≥0∞. For C above every utility this is the order-reversing change of scale between utilities and losses.

Equations

• dp.regretLoss C w a = ENNReal.ofReal (C - dp.utility w a)

@[implicit_reducible]

def Core.DecisionTheory.DecisionProblem.instMeasurableSpaceSubtypeMemFinset {A : Type u_2} (acts : Finset A) : MeasurableSpace ↥acts

Finite subtypes of actions carry the discrete σ-algebra.

Equations

• Core.DecisionTheory.DecisionProblem.instMeasurableSpaceSubtypeMemFinset acts = ⊤

theorem Core.DecisionTheory.DecisionProblem.instMeasurableSingletonClassSubtypeMemFinset {A : Type u_2} (acts : Finset A) : MeasurableSingletonClass ↥acts

theorem Core.DecisionTheory.DecisionProblem.bayesRisk_deterministic_regretLoss {W : Type u_1} {A : Type u_2} {O : Type u_3} [Fintype W] [DecidableEq W] [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype O] [DecidableEq O] [MeasurableSpace O] [MeasurableSingletonClass O] (dp : DecisionProblem ℝ W A) {acts : Finset A} (hacts : acts.Nonempty) (classify : W → O) (hprior : ∀ (w : W), 0 ≤ dp.prior w) (hsum : ∑ w : W, dp.prior w = 1) {C : ℝ} (hC : ∀ (w : W), ∀ a ∈ acts, dp.utility w a ≤ C) : ProbabilityTheory.bayesRisk (fun (w : W) (a : ↥acts) => dp.regretLoss C w ↑a) (ProbabilityTheory.Kernel.deterministic classify ⋯) dp.priorMeasure = ENNReal.ofReal (C - ∑ o : O, dp.cellProbability {x : W | classify x = o} * dp.condValue acts {x : W | classify x = o})

Utility–loss duality: for a classifier classify : W → O, the Bayes risk of the deterministic experiment "observe the cell of w" under the regret loss at C, with actions restricted to acts, is C minus the partition's decision value ∑_o P(o)·V(D ∣ fiber o). The optimal estimator is best-action-per-cell, and mathlib's bayesRisk and [vR03a]'s conditional value compute the same quantity on opposite scales.

theorem Core.DecisionTheory.DecisionProblem.questionUtility_comp_le {W : Type u_1} {A : Type u_2} {O : Type u_3} {O' : Type u_4} [Fintype W] [DecidableEq W] [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype O] [DecidableEq O] [MeasurableSpace O] [MeasurableSingletonClass O] [Fintype O'] [DecidableEq O'] [MeasurableSpace O'] [MeasurableSingletonClass O'] (dp : DecisionProblem ℝ W A) {acts : Finset A} (hacts : acts.Nonempty) (classify : W → O) (ψ : O → O') (hprior : ∀ (w : W), 0 ≤ dp.prior w) (hsum : ∑ w : W, dp.prior w = 1) (hfib : ∀ (o : O), {x : W | classify x = o}.Nonempty) (hfib' : ∀ (o' : O'), {w : W | ψ (classify w) = o'}.Nonempty) : dp.questionUtility acts (Finset.image (fun (o' : O') => {w : W | ψ (classify w) = o'}) Finset.univ) ≤ dp.questionUtility acts (Finset.image (fun (o : O) => {x : W | classify x = o}) Finset.univ)

[vR03a] §4.1, forward direction, from the Blackwell order: coarsening the classifier by post-composition cannot raise question utility. The partition instance of bayesRisk_deterministic_le_deterministic_comp, transported along the duality.

theorem Core.DecisionTheory.DecisionProblem.factorsThrough_of_forall_questionUtility_le {W : Type u_1} {O : Type u_3} {O' : Type u_4} [Fintype W] [DecidableEq W] [Nonempty W] [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype O] [DecidableEq O] [MeasurableSpace O] [MeasurableSingletonClass O] [Fintype O'] [DecidableEq O'] [MeasurableSpace O'] [MeasurableSingletonClass O'] [Nonempty O'] (f : W → O) (g : W → O') (h : ∀ (dp : DecisionProblem ℝ W O'), (∀ (w : W), 0 ≤ dp.prior w) → ∑ w : W, dp.prior w = 1 → dp.questionUtility Finset.univ (Finset.image (fun (o' : O') => {x : W | g x = o'}) Finset.univ) ≤ dp.questionUtility Finset.univ (Finset.image (fun (o : O) => {x : W | f x = o}) Finset.univ)) : ∃ (ψ : O → O'), g = ψ ∘ f

[vR03a] §4.1, converse direction (Blackwell–Sherman–Stein): if the partition of g has question utility dominated by that of f in every decision problem over action space O', then g factors through f — the coarse question is genuinely a coarsening. Chains the utility–loss duality against isGarblingOf_of_bayesRisk_uniform_le (only finite losses at the uniform prior are needed) and the deterministic-factoring characterization Kernel.deterministic_isGarblingOf_deterministic_iff.