Decision problems and the value of information

Finite decision problems over an arbitrary LinearOrdered Field K and [vR03a]'s decision-theoretic values of propositions and questions: expected utility, utility value UV, question utility EUV, value of sample information VSI/EVSI, and the maximin analogues. Theory-neutral: no question-semantic imports, so any module (RSA, causal decision theory, explanation models) can use decision problems without pulling in the Question cone.

Main definitions

• DecisionProblem: a utility function W → A → K with a prior W → K. The structure itself is constraint-free; theorems assume [Field K] [LinearOrder K] [IsStrictOrderedRing K]. Studies instantiate K := ℚ for exact, decide-friendly arithmetic; Core.Probability.Decision.ExperimentDesign uses K := ℝ against eig.
• DecisionProblem.expectedUtility, .value, .condExpectedUtility, .condValue, .utilityValue: EU(a), V(D), EU(a ∣ C), V(D ∣ C), and UV(C) = V(D ∣ C) − V(D).
• DecisionProblem.questionUtility: EUV(Q) = ∑_{q ∈ Q} P(q) · UV(q).
• DecisionProblem.valueSampleInfo, .expectedValueSampleInfo: [vR03a]'s VSI/EVSI (p. 742).
• DecisionProblem.securityLevel, .maximinValue, .maximinUtilityValue, .questionMaximin: the maximin (worst-case) analogues.
• DecisionProblem.IsResolved: [vR03a]'s resolution of a decision problem (p. 736).

Main results

• DecisionProblem.questionUtility_eq_expectedValueSampleInfo: EUV(Q) = EVSI(Q) ([vR03a], p. 742).
• DecisionProblem.questionUtility_mono_of_refines: EUV is monotone under partition refinement — the ⟹ direction of [vR03a]'s §4.1 Fact (p. 743).
• DecisionProblem.binary_question_value_decomposition: the yes/no-question instance.

Design: Fintype + Finset

Functions that sum over the full universe use [Fintype W] with ∑ w : W. Functions that operate over action sets or world subsets use Finset. questionUtility and expectedValueSampleInfo take Finset (Finset W) (cells as sets); questionMaximin takes a List (Finset W) of cells. Empty action sets get the junk value 0 (the Real.sSup convention), with _of_nonempty characterization lemmas as the working API.

• [vR03a]. Questioning to Resolve Decision Problems. L&P 26.
• [Bla53]. Equivalent Comparisons of Experiments.

structure Core.DecisionTheory.DecisionProblem (K : Type u_4) (W : Type u_5) (A : Type u_6) : Type (max (max u_4 u_5) u_6)

A decision problem D = (W, A, U, π) with utility and prior.

• utility : W → A → K

  Utility of action a in world w.

• prior : W → K

  Prior beliefs over worlds (should sum to 1 for proper probability).

def Core.DecisionTheory.DecisionProblem.uniformPrior {K : Type u_1} {W : Type u_2} [Field K] [Fintype W] : W → K

The uniform prior over a Fintype of worlds (0 when W is empty, since 1 / 0 = 0 in a field).

Equations

• Core.DecisionTheory.DecisionProblem.uniformPrior x✝ = 1 / ↑(Fintype.card W)

def Core.DecisionTheory.DecisionProblem.withUniformPrior {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [Fintype W] (utility : W → A → K) : DecisionProblem K W A

Create a decision problem with uniform prior.

Equations

• Core.DecisionTheory.DecisionProblem.withUniformPrior utility = { utility := utility, prior := Core.DecisionTheory.DecisionProblem.uniformPrior }

Expected utility

def Core.DecisionTheory.DecisionProblem.expectedUtility {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] (dp : DecisionProblem K W A) [Fintype W] (a : A) : K

Expected utility of action a given the prior.

Equations

• dp.expectedUtility a = ∑ w : W, dp.prior w * dp.utility w a

def Core.DecisionTheory.DecisionProblem.value {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) [Fintype W] (actions : Finset A) : K

Value of a decision problem: max EU over actions, or 0 if empty.

Equations

• dp.value actions = if h : actions.Nonempty then actions.sup' h dp.expectedUtility else 0

def Core.DecisionTheory.DecisionProblem.condExpectedUtility {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) (cell : Finset W) (a : A) : K

Conditional expected utility of action a given cell membership (0 on zero-mass cells).

Equations

• dp.condExpectedUtility cell a = if cell.sum dp.prior = 0 then 0 else ∑ w ∈ cell, dp.prior w / cell.sum dp.prior * dp.utility w a

def Core.DecisionTheory.DecisionProblem.condValue {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) (actions : Finset A) (cell : Finset W) : K

Value of the decision problem after learning cell: best conditional EU among actions.

Equations

• dp.condValue actions cell = if h : actions.Nonempty then actions.sup' h (dp.condExpectedUtility cell) else 0

def Core.DecisionTheory.DecisionProblem.utilityValue {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) [Fintype W] (actions : Finset A) (cell : Finset W) : K

UV(C) = V(D ∣ C) − V(D), the utility value of learning proposition C.

Equations

• dp.utilityValue actions cell = dp.condValue actions cell - dp.value actions

def Core.DecisionTheory.DecisionProblem.cellProbability {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] (dp : DecisionProblem K W A) (cell : Finset W) : K

Probability of a cell of the partition.

Equations

• dp.cellProbability cell = cell.sum dp.prior

theorem Core.DecisionTheory.DecisionProblem.value_of_nonempty {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] {dp : DecisionProblem K W A} {actions : Finset A} [Fintype W] (h : actions.Nonempty) : dp.value actions = actions.sup' h dp.expectedUtility

@[simp]

theorem Core.DecisionTheory.DecisionProblem.value_empty {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] {dp : DecisionProblem K W A} [Fintype W] : dp.value ∅ = 0

theorem Core.DecisionTheory.DecisionProblem.condValue_of_nonempty {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] {dp : DecisionProblem K W A} {actions : Finset A} {cell : Finset W} (h : actions.Nonempty) : dp.condValue actions cell = actions.sup' h (dp.condExpectedUtility cell)

@[simp]

theorem Core.DecisionTheory.DecisionProblem.condValue_empty {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] {dp : DecisionProblem K W A} {cell : Finset W} : dp.condValue ∅ cell = 0

theorem Core.DecisionTheory.DecisionProblem.condExpectedUtility_of_ne_zero {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] {dp : DecisionProblem K W A} {cell : Finset W} (h : cell.sum dp.prior ≠ 0) (a : A) : dp.condExpectedUtility cell a = ∑ w ∈ cell, dp.prior w / cell.sum dp.prior * dp.utility w a

@[simp]

theorem Core.DecisionTheory.DecisionProblem.condExpectedUtility_of_eq_zero {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] {dp : DecisionProblem K W A} {cell : Finset W} (h : cell.sum dp.prior = 0) (a : A) : dp.condExpectedUtility cell a = 0

Maximin

def Core.DecisionTheory.DecisionProblem.securityLevel {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) (worlds : Finset W) (a : A) : K

S(a) = min_w U(w, a), the security level of action a.

Equations

• dp.securityLevel worlds a = if h : worlds.Nonempty then worlds.inf' h fun (w : W) => dp.utility w a else 0

def Core.DecisionTheory.DecisionProblem.maximinValue {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) (worlds : Finset W) (actions : Finset A) : K

MV = max_a min_w U(w, a), the maximin value.

Equations

• dp.maximinValue worlds actions = if h : actions.Nonempty then actions.sup' h (dp.securityLevel worlds) else 0

theorem Core.DecisionTheory.DecisionProblem.securityLevel_of_nonempty {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] {dp : DecisionProblem K W A} {worlds : Finset W} {a : A} (h : worlds.Nonempty) : dp.securityLevel worlds a = worlds.inf' h fun (w : W) => dp.utility w a

theorem Core.DecisionTheory.DecisionProblem.maximinValue_of_nonempty {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] {dp : DecisionProblem K W A} {worlds : Finset W} {actions : Finset A} (h : actions.Nonempty) : dp.maximinValue worlds actions = actions.sup' h (dp.securityLevel worlds)

@[simp]

theorem Core.DecisionTheory.DecisionProblem.maximinValue_empty {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] {dp : DecisionProblem K W A} {worlds : Finset W} : dp.maximinValue worlds ∅ = 0

def Core.DecisionTheory.DecisionProblem.condSecurityLevel {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) [DecidableEq W] (worlds : Finset W) (a : A) (c : Finset W) : K

Conditional security level: worst case within cell c.

Equations

• dp.condSecurityLevel worlds a c = dp.securityLevel (worlds ∩ c) a

def Core.DecisionTheory.DecisionProblem.condMaximinValue {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) [DecidableEq W] (worlds : Finset W) (actions : Finset A) (c : Finset W) : K

Maximin value after learning c.

Equations

• dp.condMaximinValue worlds actions c = dp.maximinValue (worlds ∩ c) actions

def Core.DecisionTheory.DecisionProblem.maximinUtilityValue {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) [DecidableEq W] (worlds : Finset W) (actions : Finset A) (c : Finset W) : K

Maximin utility value of learning c.

Equations

• dp.maximinUtilityValue worlds actions c = dp.condMaximinValue worlds actions c - dp.maximinValue worlds actions

Resolution

def Core.DecisionTheory.DecisionProblem.IsResolved {K : Type u_1} {W : Type u_2} {A : Type u_3} [LinearOrder K] (dp : DecisionProblem K W A) (acts : Set A) (c : Set W) : Prop

c resolves decision problem (dp, acts): some action in acts weakly dominates every other action on every world in c ([vR03a], p. 736).

Equations

• dp.IsResolved acts c = ∃ a ∈ acts, ∀ b ∈ acts, ∀ w ∈ c, dp.utility w b ≤ dp.utility w a

@[implicit_reducible]

instance Core.DecisionTheory.DecisionProblem.IsResolved.instDecidable {K : Type u_1} {W : Type u_2} {A : Type u_3} [LinearOrder K] (dp : DecisionProblem K W A) (acts : Set A) (c : Set W) [Fintype A] [DecidablePred fun (x : A) => x ∈ acts] [Fintype W] [DecidablePred fun (x : W) => x ∈ c] : Decidable (dp.IsResolved acts c)

Decidability of IsResolved under finite, decidable carriers — the prerequisite for decide-based evaluation in worked study examples.

Equations

• Core.DecisionTheory.DecisionProblem.IsResolved.instDecidable dp acts c = id inferInstance

Question utility

def Core.DecisionTheory.DecisionProblem.questionUtility {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [Fintype W] (dp : DecisionProblem K W A) (actions : Finset A) (cells : Finset (Finset W)) : K

EUV(Q) = ∑_{q ∈ Q} P(q) · UV(q), the expected utility value of question Q.

Equations

• dp.questionUtility actions cells = ∑ cell ∈ cells, dp.cellProbability cell * dp.utilityValue actions cell

def Core.DecisionTheory.DecisionProblem.questionMaximin {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [DecidableEq W] (dp : DecisionProblem K W A) (worlds : Finset W) (actions : Finset A) (q : List (Finset W)) : K

MV(Q) = min_{q ∈ Q} MV(q), the maximin question value.

Equations

• dp.questionMaximin worlds actions [] = 0
• dp.questionMaximin worlds actions (c :: cs) = List.foldl (fun (m : K) (cell : Finset W) => min m (dp.maximinUtilityValue worlds actions cell)) (dp.maximinUtilityValue worlds actions c) cs

Value of sample information

noncomputable def Core.DecisionTheory.DecisionProblem.optimalAction {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [Fintype W] (dp : DecisionProblem K W A) (actions : Finset A) : Option A

Optimal action: the one with highest expected utility.

Noncomputable because it extracts a witness from an existential (Finset.exists_max_image via Classical.choice).

Equations

• dp.optimalAction actions = if h : actions.Nonempty then some ⋯.choose else none

noncomputable def Core.DecisionTheory.DecisionProblem.valueSampleInfo {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [Fintype W] (dp : DecisionProblem K W A) (actions : Finset A) (cell : Finset W) : K

VSI(C) = V(D ∣ C) − EU(a⁰ ∣ C): the value of sample information from learning proposition C, where a⁰ is the current optimal action.

Unlike UV(C) = V(D ∣ C) − V(D), VSI is always non-negative: learning C before choosing can never hurt relative to the current best action applied within C ([vR03a], p. 742).

Equations

• dp.valueSampleInfo actions cell = dp.condValue actions cell - match dp.optimalAction actions with | some a => dp.condExpectedUtility cell a | none => 0

noncomputable def Core.DecisionTheory.DecisionProblem.expectedValueSampleInfo {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [Fintype W] (dp : DecisionProblem K W A) (actions : Finset A) (cells : Finset (Finset W)) : K

EVSI(Q) = ∑ P(C) · VSI(C): the expected value of sample information from asking question Q ([vR03a], p. 742).

Equations

• dp.expectedValueSampleInfo actions cells = ∑ cell ∈ cells, dp.cellProbability cell * dp.valueSampleInfo actions cell

theorem Core.DecisionTheory.DecisionProblem.questionUtility_eq_expectedValueSampleInfo {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [Fintype W] (dp : DecisionProblem K W A) (actions : Finset A) (cells : Finset (Finset W)) (hLTE : ∀ (a : A), ∑ cell ∈ cells, dp.cellProbability cell * dp.condExpectedUtility cell a = dp.expectedUtility a) (hSum : ∑ cell ∈ cells, dp.cellProbability cell = 1) : dp.questionUtility actions cells = dp.expectedValueSampleInfo actions cells

EUV(Q) = EVSI(Q): the expected utility value of a question equals its expected value of sample information.

[vR03a], p. 742: "The expected utility value of a question is equal to its expected value of sample information."

The two hypotheses are the law of total expectation (∑ P(C) · EU(a ∣ C) = EU(a) for all actions) and cell probability normalization (∑ P(C) = 1).

Refinement monotonicity (Blackwell forward direction / [vR03a] §4.1)

[vR03a] p. 743 states that Q ⊑ Q' ↔ ∀ DP, EUV(Q) ≥ EUV(Q') is "a special case of [Bla53]". The ⟹ ("only if") direction is the data-processing / Jensen inequality: a finer question can only raise question utility. We prove it directly at the questionUtility level; the kernel-level fact it specializes — coarsening a deterministic classifier is a Markov garbling, so the finer partition has lower Bayes risk in every decision problem — is ProbabilityTheory.bayesRisk_deterministic_le_deterministic_comp in Core.Probability.Decision.Blackwell, and eig_deterministicObs_eq_euv in Core.Probability.Decision.ExperimentDesign identifies questionUtility with the expected value of the corresponding deterministic experiment.

The mathematical core is the unnormalized cell value maxₐ ∑_{w∈c} P(w)·U(w,a), which equals P(c)·V(D|c) (cellProbability_mul_condValue_eq_uValue) and is superadditive under splitting a cell into disjoint pieces (uValue_union_le): the max of a sum is at most the sum of the maxes. Summed over a partition, this gives questionUtility (finer) ≥ questionUtility (coarser).

theorem Core.DecisionTheory.DecisionProblem.cellProbability_mul_condValue_union_le {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [DecidableEq W] (dp : DecisionProblem K W A) (acts : Finset A) {c₁ c₂ : Finset W} (hdisj : Disjoint c₁ c₂) (hprior : ∀ (w : W), 0 ≤ dp.prior w) : dp.cellProbability (c₁ ∪ c₂) * dp.condValue acts (c₁ ∪ c₂) ≤ dp.cellProbability c₁ * dp.condValue acts c₁ + dp.cellProbability c₂ * dp.condValue acts c₂

Splitting a cell never decreases its decision value: for disjoint cells c₁, c₂ and a nonnegative prior, P(c₁ ∪ c₂)·V(D|c₁ ∪ c₂) ≤ P(c₁)·V(D|c₁) + P(c₂)·V(D|c₂). This is [Bla53]'s data-processing inequality for a single binary refinement, the building block of [vR03a]'s §4.1 question-utility monotonicity (p. 743).

theorem Core.DecisionTheory.DecisionProblem.questionUtility_split_ge {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [DecidableEq W] [Fintype W] (dp : DecisionProblem K W A) (acts : Finset A) {c₁ c₂ : Finset W} (rest : Finset (Finset W)) (hdisj : Disjoint c₁ c₂) (hprior : ∀ (w : W), 0 ≤ dp.prior w) (hc₁ : c₁ ∉ rest) (hc₂ : c₂ ∉ rest) (hne12 : c₁ ≠ c₂) (hcrest : c₁ ∪ c₂ ∉ rest) : dp.questionUtility acts (insert (c₁ ∪ c₂) rest) ≤ dp.questionUtility acts (insert c₁ (insert c₂ rest))

Question utility rises under refinement (binary split) — the ⟹ ("only if") direction of [vR03a]'s §4.1 Fact (p. 743), in its elementary case. Splitting one cell c₁ ∪ c₂ of a question into the two disjoint cells c₁, c₂ can only increase the expected utility value EUV. This is the finite-partition instance of [Bla53]'s data-processing inequality; any finite refinement of one partition by another is a composition of such binary splits, so iterating gives the full §4.1 monotonicity.

General partition refinement

The binary questionUtility_split_ge lifts to an arbitrary refinement of one partition by another, via general superadditivity of uValue and a fiberwise regrouping. The refinement is presented by a map assign sending each finer cell to the coarser cell containing it, with each coarser cell the union (Finset.sup) of its fiber.

theorem Core.DecisionTheory.DecisionProblem.questionUtility_mono_of_refines {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [DecidableEq W] [Fintype W] (dp : DecisionProblem K W A) (acts : Finset A) {fine coarse : Finset (Finset W)} (assign : Finset W → Finset W) (hmaps : ∀ f ∈ fine, assign f ∈ coarse) (hcover : ∀ c ∈ coarse, c = {f ∈ fine | assign f = c}.sup id) (hdisj : ∀ f₁ ∈ fine, ∀ f₂ ∈ fine, f₁ ≠ f₂ → Disjoint f₁ f₂) (hprior : ∀ (w : W), 0 ≤ dp.prior w) : dp.questionUtility acts coarse ≤ dp.questionUtility acts fine

Question utility is monotone under partition refinement — the ⟹ direction of [vR03a]'s §4.1 Fact (p. 743), in full generality. A finer partition fine (presented as a refinement of coarse via assign, with each coarse cell the disjoint union of its fiber) has EUV ≥ the coarser one. By [Bla53]: post-processing the finer experiment cannot raise the convex value. Generalizes questionUtility_split_ge.

Maximin monotonicity

Security level and maximin value are antitone in the world set: restricting to a subset can only improve worst-case guarantees.

theorem Core.DecisionTheory.DecisionProblem.securityLevel_le_utility {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) (worlds : Finset W) (a : A) {w : W} (hw : w ∈ worlds) : dp.securityLevel worlds a ≤ dp.utility w a

The security level is at most the utility of any world in the set.

theorem Core.DecisionTheory.DecisionProblem.securityLevel_anti {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) {S₁ S₂ : Finset W} (a : A) (hne : S₁.Nonempty) (hsub : S₁ ⊆ S₂) : dp.securityLevel S₂ a ≤ dp.securityLevel S₁ a

The security level is antitone in the world set: a min over fewer elements is at least the min over more.

theorem Core.DecisionTheory.DecisionProblem.maximinValue_anti {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] (dp : DecisionProblem K W A) {S₁ S₂ : Finset W} (actions : Finset A) (hne : S₁.Nonempty) (hsub : S₁ ⊆ S₂) : dp.maximinValue S₂ actions ≤ dp.maximinValue S₁ actions

The maximin value is antitone in the world set.

theorem Core.DecisionTheory.DecisionProblem.maximinUtilityValue_anti {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [DecidableEq W] (dp : DecisionProblem K W A) (worlds : Finset W) (actions : Finset A) {c₁ c₂ : Finset W} (hsub : c₁ ⊆ c₂) (hne : (worlds ∩ c₁).Nonempty) : dp.maximinUtilityValue worlds actions c₂ ≤ dp.maximinUtilityValue worlds actions c₁

Maximin utility value is antitone in the cell: learning a more specific proposition (subset of worlds) gives a higher MUV.

theorem Core.DecisionTheory.DecisionProblem.maximinUtilityValue_nonneg {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [DecidableEq W] (dp : DecisionProblem K W A) (worlds : Finset W) (actions : Finset A) (c : Finset W) (hne : (worlds ∩ c).Nonempty) : 0 ≤ dp.maximinUtilityValue worlds actions c

Maximin value of information is non-negative for nonempty cells: the maximin over worlds ∩ c ⊆ worlds considers fewer worst cases.

List minimum helpers

theorem Core.DecisionTheory.DecisionProblem.questionMaximin_le_maximinUtilityValue {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [DecidableEq W] (dp : DecisionProblem K W A) (worlds : Finset W) (actions : Finset A) (q : List (Finset W)) {cell : Finset W} (hcell : cell ∈ q) : dp.questionMaximin worlds actions q ≤ dp.maximinUtilityValue worlds actions cell

The question maximin value is at most the MUV of each cell in the question.

Special decision problems

def Core.DecisionTheory.DecisionProblem.epistemic {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [DecidableEq W] (target : W) : DecisionProblem K W A

An epistemic DP where the agent wants to know the exact world state.

Equations

• Core.DecisionTheory.DecisionProblem.epistemic target = { utility := fun (w : W) (x : A) => if w = target then 1 else 0, prior := fun (x : W) => 1 }

def Core.DecisionTheory.DecisionProblem.completeInformation {K : Type u_1} {W : Type u_2} [Field K] [DecidableEq W] : DecisionProblem K W W

A complete-information DP where only exact-state knowledge is useful.

Equations

• Core.DecisionTheory.DecisionProblem.completeInformation = { utility := fun (w a : W) => if a = w then 1 else 0, prior := fun (x : W) => 1 }

def Core.DecisionTheory.DecisionProblem.mentionSome {K : Type u_1} {W : Type u_2} [Field K] (satisfies : W → Prop) [DecidablePred satisfies] : DecisionProblem K W Bool

A mention-some DP: any satisfier resolves the problem.

Equations

• Core.DecisionTheory.DecisionProblem.mentionSome satisfies = { utility := fun (w : W) (a : Bool) => if a = true ∧ satisfies w then 1 else 0, prior := fun (x : W) => 1 }

Binary question value decomposition

For a binary partition {P, ¬P}, the probability-weighted sum of conditional DP values equals Van Rooy's question utility plus the baseline DP value. This is the structural identity connecting "the value of asking a yes/no question" to the decision-theoretic question framework of [vR03a].

theorem Core.DecisionTheory.DecisionProblem.cellProbability_filter_add_filter_not {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [Fintype W] [DecidableEq W] (dp : DecisionProblem K W A) (P : W → Prop) [DecidablePred P] (hPrior : Finset.univ.sum dp.prior = 1) : dp.cellProbability (Finset.filter P Finset.univ) + dp.cellProbability {x : W | ¬P x} = 1

Cell probabilities of a binary partition {P, ¬P} sum to 1 when the prior is a proper distribution.

theorem Core.DecisionTheory.DecisionProblem.binary_question_value_decomposition {K : Type u_1} {W : Type u_2} {A : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Fintype W] [DecidableEq W] (dp : DecisionProblem K W A) (actions : Finset A) (P : W → Prop) [DecidablePred P] (hPrior : Finset.univ.sum dp.prior = 1) : dp.cellProbability (Finset.filter P Finset.univ) * dp.condValue actions (Finset.filter P Finset.univ) + dp.cellProbability {x : W | ¬P x} * dp.condValue actions {x : W | ¬P x} = dp.questionUtility actions {Finset.filter P Finset.univ, {x : W | ¬P x}} + dp.value actions

Binary question value decomposition: for a binary partition {P, ¬P},

`∑ P(cell) · V(D|cell) = EUV({P, ¬P}, D) + V(D)`

where the LHS is the probability-weighted sum of conditional DP values, EUV is questionUtility, and V(D) is value.