Admissible actions in finite decision problems

A decision problem without data has parameters Θ, actions 𝓨 and a loss ℓ : Θ → 𝓨 → ℝ≥0∞. A randomized action ν is the estimator Kernel.const Unit ν for the data kernel Kernel.discard Θ, which observes nothing, and its risk at θ is ∫⁻ y, ℓ θ y ∂ν. With finitely many parameters and actions and finite losses, being a Bayes action and escaping domination coincide. An action is a Bayes estimator for some prior iff no randomized action has smaller risk at every parameter, and it is admissible iff it is a Bayes estimator for a prior that charges every parameter, the complete class theorem. Both come from theorems of the alternative for the matrix of risk differences. Against nature in game theory these are Pearce's lemmas, an act that is never a best response is strictly dominated and an act that no mixture weakly dominates is a best response to a belief of full support, and the payoff versions state them for utilities. [UPSTREAM] candidate for Mathlib/Probability/Decision/.

Main definitions

• ProbabilityTheory.IsStrictlyDominated: another randomized action has smaller risk at every parameter.
• ProbabilityTheory.IsAdmissible: no randomized action has risk at most as large everywhere and smaller somewhere.

Main statements

• ProbabilityTheory.exists_isBayesEstimator_iff_not_isStrictlyDominated: an action is Bayes for some prior iff it is not strictly dominated.
• ProbabilityTheory.isAdmissible_iff_exists_isBayesEstimator: an action is admissible iff it is Bayes for a prior of full support.
• ProbabilityTheory.exists_maximizesPayoff_iff_not_isStrictlyPayoffDominated, ProbabilityTheory.not_isWeaklyPayoffDominated_iff_exists_maximizesPayoff: the payoff versions, Pearce's lemmas.

References

• [Pea84]

Helpers on finite types

Dominance and admissibility

def ProbabilityTheory.IsStrictlyDominated {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] (ℓ : Θ → 𝓨 → ENNReal) (ν : MeasureTheory.Measure 𝓨) : Prop

A randomized action is strictly dominated when another has smaller risk at every parameter.

Equations

• ProbabilityTheory.IsStrictlyDominated ℓ ν = ∃ (ν' : MeasureTheory.Measure 𝓨), MeasureTheory.IsProbabilityMeasure ν' ∧ ∀ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂ν' < ∫⁻ (y : 𝓨), ℓ θ y ∂ν

def ProbabilityTheory.IsAdmissible {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] (ℓ : Θ → 𝓨 → ENNReal) (ν : MeasureTheory.Measure 𝓨) : Prop

A randomized action is admissible when every action whose risk is nowhere larger has the same risk everywhere.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.mixedPayoff {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] (U : 𝓨 → Θ → ℝ) (ν : MeasureTheory.Measure 𝓨) (θ : Θ) : ℝ

The payoff of the randomized action ν at the parameter θ.

Equations

• ProbabilityTheory.mixedPayoff U ν θ = ∫ (y : 𝓨), U y θ ∂ν

def ProbabilityTheory.IsStrictlyPayoffDominated {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] (U : 𝓨 → Θ → ℝ) (ν : MeasureTheory.Measure 𝓨) : Prop

ν is strictly dominated in payoff when another randomized action pays more at every parameter.

Equations

• One or more equations did not get rendered due to their size.

def ProbabilityTheory.IsWeaklyPayoffDominated {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] (U : 𝓨 → Θ → ℝ) (ν : MeasureTheory.Measure 𝓨) : Prop

ν is weakly dominated in payoff when another randomized action pays at least as much at every parameter and more at some.

Equations

• One or more equations did not get rendered due to their size.

Risks and payoffs on reals

theorem ProbabilityTheory.mixedPayoff_eq_sum {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] [Fintype 𝓨] [MeasurableSingletonClass 𝓨] (U : 𝓨 → Θ → ℝ) (ν : MeasureTheory.Measure 𝓨) [MeasureTheory.IsFiniteMeasure ν] (θ : Θ) : mixedPayoff U ν θ = ∑ y : 𝓨, ν.real {y} * U y θ

Bayes actions

noncomputable def ProbabilityTheory.expectedPayoff {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] [MeasurableSpace Θ] (U : 𝓨 → Θ → ℝ) (P : MeasureTheory.Measure Θ) (ν : MeasureTheory.Measure 𝓨) : ℝ

The expected payoff of the randomized action ν under the belief P.

Equations

• ProbabilityTheory.expectedPayoff U P ν = ∫ (θ : Θ), ProbabilityTheory.mixedPayoff U ν θ ∂P

def ProbabilityTheory.MaximizesPayoff {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] [MeasurableSpace Θ] (U : 𝓨 → Θ → ℝ) (P : MeasureTheory.Measure Θ) (ν : MeasureTheory.Measure 𝓨) : Prop

ν maximizes the expected payoff under P among the randomized actions.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.isBayesEstimator_discard_const_iff {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] [MeasurableSpace Θ] {ℓ : Θ → 𝓨 → ENNReal} {ν : MeasureTheory.Measure 𝓨} [MeasureTheory.IsProbabilityMeasure ν] {π : MeasureTheory.Measure Θ} : IsBayesEstimator ℓ (Kernel.discard Θ) (Kernel.const Unit ν) π ↔ ∀ (ν' : MeasureTheory.Measure 𝓨), MeasureTheory.IsProbabilityMeasure ν' → ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂ν ∂π ≤ ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂ν' ∂π

Without data, a randomized action is a Bayes estimator for π iff no randomized action has smaller average risk.

theorem ProbabilityTheory.expectedPayoff_eq_sum {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] [MeasurableSpace Θ] [Fintype Θ] [MeasurableSingletonClass Θ] (U : 𝓨 → Θ → ℝ) (P : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure P] (ν : MeasureTheory.Measure 𝓨) : expectedPayoff U P ν = ∑ θ : Θ, P.real {θ} * mixedPayoff U ν θ

theorem ProbabilityTheory.expectedPayoff_lt_of_forall_lt {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] [MeasurableSpace Θ] [Fintype Θ] [MeasurableSingletonClass Θ] (U : 𝓨 → Θ → ℝ) (P : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure P] {ν ν' : MeasureTheory.Measure 𝓨} (h : ∀ (θ : Θ), mixedPayoff U ν θ < mixedPayoff U ν' θ) : expectedPayoff U P ν < expectedPayoff U P ν'

A randomized action that pays more at every parameter has a larger expected payoff under every belief.

Strict dominance and Bayes actions

theorem ProbabilityTheory.exists_isBayesEstimator_iff_not_isStrictlyDominated {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] [MeasurableSpace Θ] [Fintype Θ] [MeasurableSingletonClass Θ] [Fintype 𝓨] [MeasurableSingletonClass 𝓨] {ℓ : Θ → 𝓨 → ENNReal} (hℓ : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≠ ⊤) (ν : MeasureTheory.Measure 𝓨) [MeasureTheory.IsProbabilityMeasure ν] : (∃ (π : MeasureTheory.Measure Θ), MeasureTheory.IsProbabilityMeasure π ∧ IsBayesEstimator ℓ (Kernel.discard Θ) (Kernel.const Unit ν) π) ↔ ¬IsStrictlyDominated ℓ ν

In a finite decision problem, a randomized action is a Bayes estimator for some prior iff no randomized action has smaller risk at every parameter. This is Pearce's lemma.

Admissibility and the complete class theorem

theorem ProbabilityTheory.isAdmissible_iff_exists_isBayesEstimator {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] [MeasurableSpace Θ] [Fintype Θ] [MeasurableSingletonClass Θ] [Fintype 𝓨] [MeasurableSingletonClass 𝓨] {ℓ : Θ → 𝓨 → ENNReal} (hℓ : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≠ ⊤) [Nonempty Θ] (ν : MeasureTheory.Measure 𝓨) [MeasureTheory.IsProbabilityMeasure ν] : IsAdmissible ℓ ν ↔ ∃ (π : MeasureTheory.Measure Θ), MeasureTheory.IsProbabilityMeasure π ∧ (∀ (θ : Θ), π {θ} ≠ 0) ∧ IsBayesEstimator ℓ (Kernel.discard Θ) (Kernel.const Unit ν) π

Complete class theorem. In a finite decision problem, a randomized action is admissible iff it is a Bayes estimator for a prior that charges every parameter.

Payoffs

A payoff table U : 𝓨 → Θ → ℝ is a loss with the sign reversed: the regret C − U at a bound C on the payoffs ranks randomized actions as their payoffs do, the other way round.

theorem ProbabilityTheory.exists_maximizesPayoff_iff_not_isStrictlyPayoffDominated {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] [MeasurableSpace Θ] [Fintype Θ] [MeasurableSingletonClass Θ] [Fintype 𝓨] [MeasurableSingletonClass 𝓨] (U : 𝓨 → Θ → ℝ) (ν : MeasureTheory.Measure 𝓨) [MeasureTheory.IsProbabilityMeasure ν] : (∃ (P : MeasureTheory.Measure Θ), MeasureTheory.IsProbabilityMeasure P ∧ MaximizesPayoff U P ν) ↔ ¬IsStrictlyPayoffDominated U ν

A randomized action maximizes the expected payoff under some belief iff no randomized action pays more at every parameter. This is Pearce's lemma for payoffs.

theorem ProbabilityTheory.not_isWeaklyPayoffDominated_iff_exists_maximizesPayoff {Θ : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓨] [MeasurableSpace Θ] [Fintype Θ] [MeasurableSingletonClass Θ] [Fintype 𝓨] [MeasurableSingletonClass 𝓨] (U : 𝓨 → Θ → ℝ) [Nonempty Θ] (ν : MeasureTheory.Measure 𝓨) [MeasureTheory.IsProbabilityMeasure ν] : ¬IsWeaklyPayoffDominated U ν ↔ ∃ (P : MeasureTheory.Measure Θ), MeasureTheory.IsProbabilityMeasure P ∧ (∀ (θ : Θ), P {θ} ≠ 0) ∧ MaximizesPayoff U P ν

A randomized action that no randomized action weakly dominates in payoff maximizes the expected payoff under a belief of full support, and conversely. This is Pearce's lemma for weak dominance.