The value of information of an experiment

An experiment is a Markov kernel κ : Kernel Θ 𝓧 that draws an observation from a parameter. An agent with prior π who values a belief μ at V μ expects, before observing, the value of the posterior κ†π; the value of information valueOfInformation V κ π is that expectation less the value of the prior. DeGroot calls it the information in the experiment when V is the negative of an uncertainty function, and Lindley's measure of information is the case of Shannon entropy.

The decision value decisionValue U μ of a belief is the best expected utility of an action. For it, the value of information is the risk increase of mathlib's decision theory at the regret loss C − U, so information never has negative value, and garbling an experiment never raises its value, the forward direction of Blackwell's comparison of experiments. For an experiment that observes a classifier f, the value of information is the probability-weighted value of the prior conditioned on each fibre of f; a fixed statistic gains nothing, which is the law of total expectation over the fibres, and the converse of Blackwell's theorem says that a classifier never worth more than f factors through f. Observing the parameter itself leaves a point-mass belief, so its value is the expected value of perfect information, and no experiment is worth more.

Main definitions

• valueOfInformation V κ π: the expected value of the posterior less the value of the prior.
• decisionValue U μ: the best expected utility of an action under the belief μ.

Main statements

• hasArgminEstimator_of_finite: with countably many observations and finitely many actions, a pointwise minimizer of the posterior expected loss is an argmin estimator.
• riskIncrease_ofReal_sub: at the regret loss, the risk increase is the value of information of the decision value.
• valueOfInformation_decisionValue_nonneg: information has nonnegative value.
• valueOfInformation_decisionValue_comp_le: a garbled experiment is worth no more.
• valueOfInformation_const: an experiment whose law does not depend on the parameter is worth nothing.
• valueOfInformation_deterministic, sum_measureReal_mul_integral_cond: the value of observing a classifier sums over its fibres, and the law of total expectation over them.
• exists_eq_comp_of_forall_valueOfInformation_le: a classifier never worth more than f factors through f.
• valueOfInformation_id, valueOfInformation_decisionValue_le_id: observing the parameter is worth the expected value of its point-mass beliefs, and no experiment is worth more.

Implementation notes

The decision value is a supremum over the action type, 0 when there is no action. The theorems about it assume finitely many parameters, observations and actions, and the regret bound C stays inside the proofs of the inequalities.

References

• [DeG62]
• [Lin56]
• [Bla53]
• [RS61]

theorem ProbabilityTheory.hasArgminEstimator_of_finite {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace Θ] [Nonempty Θ] [Countable 𝓧] [MeasurableSingletonClass 𝓧] [Finite 𝓨] [Nonempty 𝓨] (ℓ : Θ → 𝓨 → ENNReal) (P : Kernel Θ 𝓧) [IsFiniteKernel P] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] : HasArgminEstimator ℓ P π

With countably many observations and finitely many estimates, choosing a minimizer of the posterior expected loss at each observation gives an argmin estimator.

theorem MeasureTheory.Measure.integral_comp {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure 𝓧} {κ : ProbabilityTheory.Kernel 𝓧 Θ} {f : Θ → E} (hf : Integrable f (μ.bind ⇑κ)) : ∫ (θ : Θ), f θ ∂μ.bind ⇑κ = ∫ (x : 𝓧), ∫ (θ : Θ), f θ ∂κ x ∂μ

Integrating against the composition of a kernel with a measure integrates twice.

noncomputable def ProbabilityTheory.valueOfInformation {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [StandardBorelSpace Θ] [Nonempty Θ] (V : MeasureTheory.Measure Θ → ℝ) (κ : Kernel Θ 𝓧) [IsFiniteKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] : ℝ

The value of information of the experiment κ to an agent with prior π who values a belief by V is the expected value of the posterior less the value of the prior.

Equations

• ProbabilityTheory.valueOfInformation V κ π = ∫ (x : 𝓧), V ((ProbabilityTheory.posterior κ π) x) ∂π.bind ⇑κ - V π

noncomputable def ProbabilityTheory.decisionValue {Θ : Type u_1} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} (U : Θ → 𝓨 → ℝ) (μ : MeasureTheory.Measure Θ) : ℝ

The decision value of a belief μ is the best expected utility of an action under μ.

Equations

• ProbabilityTheory.decisionValue U μ = ⨆ (a : 𝓨), ∫ (θ : Θ), U θ a ∂μ

theorem ProbabilityTheory.valueOfInformation_smul {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [StandardBorelSpace Θ] [Nonempty Θ] (κ : Kernel Θ 𝓧) [IsFiniteKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] (V : MeasureTheory.Measure Θ → ℝ) (c : ℝ) : valueOfInformation (c • V) κ π = c * valueOfInformation V κ π

theorem ProbabilityTheory.valueOfInformation_const {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [StandardBorelSpace Θ] [Nonempty Θ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] (V : MeasureTheory.Measure Θ → ℝ) (ν : MeasureTheory.Measure 𝓧) [MeasureTheory.IsProbabilityMeasure ν] [MeasureTheory.IsProbabilityMeasure π] : valueOfInformation V (Kernel.const Θ ν) π = 0

An experiment whose law does not depend on the parameter is worth nothing.

theorem ProbabilityTheory.valueOfInformation_id {Θ : Type u_1} {mΘ : MeasurableSpace Θ} [StandardBorelSpace Θ] [Nonempty Θ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] (V : MeasureTheory.Measure Θ → ℝ) : valueOfInformation V Kernel.id π = ∫ (θ : Θ), V (MeasureTheory.Measure.dirac θ) ∂π - V π

Observing the parameter itself leaves a point-mass belief at each value.

theorem ProbabilityTheory.valueOfInformation_integral {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [StandardBorelSpace Θ] [Nonempty Θ] [Finite Θ] [MeasurableSingletonClass Θ] [Finite 𝓧] [MeasurableSingletonClass 𝓧] (g : Θ → ℝ) (κ : Kernel Θ 𝓧) [IsMarkovKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure π] : valueOfInformation (fun (ν : MeasureTheory.Measure Θ) => ∫ (θ : Θ), g θ ∂ν) κ π = 0

A fixed statistic gains nothing from an experiment, since the posteriors average back to the prior.

theorem ProbabilityTheory.decisionValue_smul {Θ : Type u_1} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {U : Θ → 𝓨 → ℝ} {c : ℝ} (hc : 0 ≤ c) (μ : MeasureTheory.Measure Θ) : decisionValue (c • U) μ = c * decisionValue U μ

@[simp]

theorem ProbabilityTheory.decisionValue_dirac {Θ : Type u_1} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {U : Θ → 𝓨 → ℝ} [MeasurableSingletonClass Θ] (θ : Θ) : decisionValue U (MeasureTheory.Measure.dirac θ) = ⨆ (a : 𝓨), U θ a

theorem ProbabilityTheory.integral_le_decisionValue {Θ : Type u_1} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {U : Θ → 𝓨 → ℝ} [Finite 𝓨] (μ : MeasureTheory.Measure Θ) (a : 𝓨) : ∫ (θ : Θ), U θ a ∂μ ≤ decisionValue U μ

The decision value and the risk increase

theorem ProbabilityTheory.decisionValue_le {Θ : Type u_1} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} [Finite Θ] [MeasurableSingletonClass Θ] [Nonempty 𝓨] {U : Θ → 𝓨 → ℝ} {C : ℝ} (hC : ∀ (θ : Θ) (a : 𝓨), U θ a ≤ C) (μ : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure μ] : decisionValue U μ ≤ C

theorem ProbabilityTheory.iInf_lintegral_ofReal_sub {Θ : Type u_1} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} [Finite Θ] [MeasurableSingletonClass Θ] [Finite 𝓨] [Nonempty 𝓨] {U : Θ → 𝓨 → ℝ} {C : ℝ} (hC : ∀ (θ : Θ) (a : 𝓨), U θ a ≤ C) (μ : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure μ] : ⨅ (a : 𝓨), ∫⁻ (θ : Θ), ENNReal.ofReal (C - U θ a) ∂μ = ENNReal.ofReal (C - decisionValue U μ)

At a bound C on the utilities, the least expected regret C − U of an action is C less the decision value.

theorem ProbabilityTheory.bayesRisk_ofReal_sub {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [Finite Θ] [MeasurableSingletonClass Θ] [Finite 𝓨] [Nonempty 𝓨] {U : Θ → 𝓨 → ℝ} {C : ℝ} (hC : ∀ (θ : Θ) (a : 𝓨), U θ a ≤ C) [StandardBorelSpace Θ] [Nonempty Θ] [Finite 𝓧] [MeasurableSingletonClass 𝓧] (κ : Kernel Θ 𝓧) [IsMarkovKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure π] [MeasurableSpace 𝓨] [MeasurableSingletonClass 𝓨] : bayesRisk (fun (θ : Θ) (a : 𝓨) => ENNReal.ofReal (C - U θ a)) κ π = ENNReal.ofReal (C - ∫ (x : 𝓧), decisionValue U ((posterior κ π) x) ∂π.bind ⇑κ)

At the regret loss C − U, the Bayes risk of an experiment is C less the expected decision value of the posterior.

theorem ProbabilityTheory.riskIncrease_ofReal_sub {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [Finite Θ] [MeasurableSingletonClass Θ] [Finite 𝓨] [Nonempty 𝓨] {U : Θ → 𝓨 → ℝ} {C : ℝ} (hC : ∀ (θ : Θ) (a : 𝓨), U θ a ≤ C) [StandardBorelSpace Θ] [Nonempty Θ] [Finite 𝓧] [MeasurableSingletonClass 𝓧] (κ : Kernel Θ 𝓧) [IsMarkovKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure π] [MeasurableSpace 𝓨] [MeasurableSingletonClass 𝓨] : riskIncrease (fun (θ : Θ) (a : 𝓨) => ENNReal.ofReal (C - U θ a)) κ π = ENNReal.ofReal (valueOfInformation (decisionValue U) κ π)

At the regret loss C − U, the risk increase of an experiment is the value of information of the decision value.

theorem ProbabilityTheory.valueOfInformation_decisionValue_nonneg {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [Finite Θ] [MeasurableSingletonClass Θ] [StandardBorelSpace Θ] [Nonempty Θ] [Finite 𝓧] [MeasurableSingletonClass 𝓧] [Finite 𝓨] (U : Θ → 𝓨 → ℝ) (κ : Kernel Θ 𝓧) [IsMarkovKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure π] : 0 ≤ valueOfInformation (decisionValue U) κ π

Information has nonnegative value to an expected-utility maximizer.

theorem ProbabilityTheory.valueOfInformation_decisionValue_comp_le {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [Finite Θ] [MeasurableSingletonClass Θ] [StandardBorelSpace Θ] [Nonempty Θ] [Finite 𝓧] [MeasurableSingletonClass 𝓧] [Finite 𝓨] (U : Θ → 𝓨 → ℝ) (κ : Kernel Θ 𝓧) [IsMarkovKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure π] {𝓧' : Type u_4} {m𝓧' : MeasurableSpace 𝓧'} [Finite 𝓧'] [MeasurableSingletonClass 𝓧'] (η : Kernel 𝓧 𝓧') [IsMarkovKernel η] : valueOfInformation (decisionValue U) (η.comp κ) π ≤ valueOfInformation (decisionValue U) κ π

Garbling an experiment cannot raise its value to an expected-utility maximizer.

theorem ProbabilityTheory.valueOfInformation_decisionValue_le_id {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [Finite Θ] [MeasurableSingletonClass Θ] [StandardBorelSpace Θ] [Nonempty Θ] [Finite 𝓧] [MeasurableSingletonClass 𝓧] [Finite 𝓨] (U : Θ → 𝓨 → ℝ) (κ : Kernel Θ 𝓧) [IsMarkovKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure π] : valueOfInformation (decisionValue U) κ π ≤ valueOfInformation (decisionValue U) Kernel.id π

No experiment is worth more than observing the parameter itself, the expected value of perfect information.

Deterministic experiments

theorem ProbabilityTheory.valueOfInformation_deterministic {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [Finite Θ] [MeasurableSingletonClass Θ] [StandardBorelSpace Θ] [Nonempty Θ] [Fintype 𝓧] [MeasurableSingletonClass 𝓧] (V : MeasureTheory.Measure Θ → ℝ) {f : Θ → 𝓧} (hf : Measurable f) (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] : valueOfInformation V (Kernel.deterministic f hf) π = ∑ x : 𝓧, π.real (f ⁻¹' {x}) * V π[|f ⁻¹' {x}] - V π

The value of information of observing f is the decision value of the prior conditioned on each fibre of f, weighted by the fibre's probability, less the decision value of the prior.

theorem ProbabilityTheory.valueOfInformation_decisionValue_le_of_factorsThrough {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [Finite Θ] [MeasurableSingletonClass Θ] [StandardBorelSpace Θ] [Nonempty Θ] [Fintype 𝓧] [MeasurableSingletonClass 𝓧] [Finite 𝓨] (U : Θ → 𝓨 → ℝ) {𝓧' : Type u_4} {m𝓧' : MeasurableSpace 𝓧'} [Finite 𝓧'] [MeasurableSingletonClass 𝓧'] {f : Θ → 𝓧} {g : Θ → 𝓧'} (hf : Measurable f) (hg : Measurable g) (h : Function.FactorsThrough g f) (π : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure π] : valueOfInformation (decisionValue U) (Kernel.deterministic g hg) π ≤ valueOfInformation (decisionValue U) (Kernel.deterministic f hf) π

Observing a function of f is worth no more to an expected-utility maximizer than observing f.

theorem ProbabilityTheory.sum_measureReal_mul_integral_cond {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} [Finite Θ] [MeasurableSingletonClass Θ] [StandardBorelSpace Θ] [Nonempty Θ] [Fintype 𝓧] (g : Θ → ℝ) (f : Θ → 𝓧) (π : MeasureTheory.Measure Θ) [MeasureTheory.IsProbabilityMeasure π] : ∑ x : 𝓧, π.real (f ⁻¹' {x}) * ∫ (θ : Θ), g θ ∂π[|f ⁻¹' {x}] = ∫ (θ : Θ), g θ ∂π

Averaging the expectations conditional on the fibres of f recovers the expectation, the law of total expectation.

theorem ProbabilityTheory.exists_eq_comp_of_forall_valueOfInformation_le {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [Finite Θ] [MeasurableSingletonClass Θ] [StandardBorelSpace Θ] [Nonempty Θ] [Fintype 𝓧] [MeasurableSingletonClass 𝓧] {𝓧' : Type u_4} {m𝓧' : MeasurableSpace 𝓧'} [Fintype 𝓧'] [MeasurableSingletonClass 𝓧'] [Nonempty 𝓧'] [Fintype Θ] (f : Θ → 𝓧) (g : Θ → 𝓧') (h : ∀ (U : Θ → 𝓧' → ℝ), valueOfInformation (decisionValue U) (Kernel.deterministic g ⋯) (uniformOn Set.univ) ≤ valueOfInformation (decisionValue U) (Kernel.deterministic f ⋯) (uniformOn Set.univ)) : ∃ (ψ : 𝓧 → 𝓧'), g = ψ ∘ f

If observing g is never worth more than observing f to an expected-utility maximizer with actions 𝓧' and a uniform prior, then g factors through f.