Blackwell comparison of experiments

A statistical experiment is a Markov kernel P : Kernel Θ 𝓧 generating data in 𝓧 from a parameter in Θ. Experiment P is at least as informative as P' : Kernel Θ 𝓧' when P' can be recovered from P by Markov post-processing ("garbling"): P' = η ∘ₖ P for some Markov kernel η. This file develops that order and its characterization through Bayes risk.

[Bla53]'s comparison theorem states that P is at least as informative as P' if and only if, for every decision problem, the Bayes risk under P is no greater than under P'. We state and prove this equivalence over ProbabilityTheory.bayesRisk for finite spaces: the forward direction is the data-processing inequality, the converse the Blackwell–Sherman–Stein separation argument (see the implementation notes).

Main definitions

• Kernel.IsGarblingOf: P'.IsGarblingOf P means P' is a Markov garbling of P, i.e. P is at least as informative as P'. Reflexive (Kernel.IsGarblingOf.refl) and transitive (Kernel.IsGarblingOf.trans).
• Kernel.BlackwellDominates: P.BlackwellDominates P' means P has Bayes risk no greater than P' for every decision problem and prior — the dual side of the Blackwell equivalence.

Main statements

• bayesRisk_le_of_isGarblingOf / blackwellDominates_of_isGarblingOf: if P' is a garbling of P, then P Blackwell-dominates P' (the data-processing direction).
• isGarblingOf_of_blackwellDominates: conversely, if P Blackwell-dominates P', then P' is a garbling of P (the Blackwell–Sherman–Stein direction, finite case). Requires finite, nonempty Θ and that both P and P' are Markov kernels — false otherwise (see the theorem docstring for counterexamples).
• isGarblingOf_iff_blackwellDominates: the two directions combined.

Implementation notes

The development is stated entirely over Mathlib's Kernel and bayesRisk with no further dependencies, so it can serve as a Mathlib.Probability.Decision.Blackwell candidate. The finite, ℝ-valued eig / questionUtility view in Core.Probability.Decision.ExperimentDesign is a downstream consumer: eig_deterministicObs_eq_euv there identifies the deterministic- experiment value with [vR03a]'s question utility, whose refinement monotonicity is the partition instance of bayesRisk_deterministic_le_deterministic_comp below.

Kernel.BlackwellDominates quantifies over all decision problems (every measurable action space 𝓨 and loss ℓ : Θ → 𝓨 → ℝ≥0∞) and priors: dominance for a single one does not force garbling. The action-space universe is pinned to u (the universe of 𝓧') because the converse proof instantiates the dominance hypothesis at the action space 𝓨 := 𝓧' (the identity estimator).

The converse proof encodes finite kernels as real vectors of singleton masses (encode) and realizes the garblings of P as a compact convex polytope garblingSet P (the linear image of the product of standard simplices). If encode P' lies outside the polytope, the geometric Hahn–Banach theorem (geometric_hahn_banach_point_closed) yields a separating functional f; its coordinate matrix a θ x' = f (Pi.single θ (Pi.single x' 1)), shifted by a constant C to be nonnegative, defines a loss ℓ θ x' = ENNReal.ofReal (a θ x' + C) on actions 𝓧'. Under the uniform prior, the Bayes risk of any experiment Q evaluated at the identity estimator equals ENNReal.ofReal (|Θ|⁻¹ · f (encode Q) + C): the identity estimator pins P' to f (encode P'), while every estimator for P produces a garbling, whose f-value exceeds the separation level. This realizes bayesRisk ℓ P' π < bayesRisk ℓ P π, contradicting the hypothesis — no minimax theorem is needed, the infimum is bounded below directly. All analytic inputs come from Mathlib (isCompact_stdSimplex, the geometric_hahn_banach_* lemmas, bayesRisk_fintype). The kernel-to-stochastic-matrix bridge (encode, garblingMap, buildKernel) is currently private proof scaffolding; it is a self-contained finite-kernel ↔ row-stochastic-matrix correspondence that would naturally graduate to its own public file when upstreamed.

References

• [Bla53]

def ProbabilityTheory.Kernel.IsGarblingOf {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] [m𝓧' : MeasurableSpace 𝓧'] (P' : Kernel Θ 𝓧') (P : Kernel Θ 𝓧) : Prop

P' is a garbling of P (Blackwell): there is a Markov post-processing kernel η with P' = η ∘ₖ P. Read "P is at least as informative as P'".

Equations

• P'.IsGarblingOf P = ∃ (η : ProbabilityTheory.Kernel 𝓧 𝓧'), ProbabilityTheory.IsMarkovKernel η ∧ P' = η.comp P

theorem ProbabilityTheory.Kernel.IsGarblingOf.refl {Θ : Type u_1} {𝓧 : Type u_2} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] (P : Kernel Θ 𝓧) [IsMarkovKernel P] : P.IsGarblingOf P

theorem ProbabilityTheory.Kernel.IsGarblingOf.trans {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] [m𝓧' : MeasurableSpace 𝓧'] {𝓧'' : Type u_3} [MeasurableSpace 𝓧''] {P'' : Kernel Θ 𝓧''} {P' : Kernel Θ 𝓧'} {P : Kernel Θ 𝓧} (h₂ : P''.IsGarblingOf P') (h₁ : P'.IsGarblingOf P) : P''.IsGarblingOf P

def ProbabilityTheory.Kernel.BlackwellDominates {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] [m𝓧' : MeasurableSpace 𝓧'] (P : Kernel Θ 𝓧) (P' : Kernel Θ 𝓧') : Prop

P Blackwell-dominates P': for every decision problem (action space 𝓨, loss ℓ) and prior π, the Bayes risk under P is no larger than under P'. The right-hand side of the Blackwell equivalence.

Equations

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

theorem ProbabilityTheory.bayesRisk_le_of_isGarblingOf {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] [m𝓧' : MeasurableSpace 𝓧'] {𝓨 : Type u} [MeasurableSpace 𝓨] (ℓ : Θ → 𝓨 → ENNReal) {P : Kernel Θ 𝓧} {P' : Kernel Θ 𝓧'} (h : P'.IsGarblingOf P) (π : MeasureTheory.Measure Θ) : bayesRisk ℓ P π ≤ bayesRisk ℓ P' π

Easy direction (data-processing). If P' is a garbling of P, then for every decision problem the Bayes risk under P is no larger than under P': garbling the more-informative experiment cannot help. Specializes bayesRisk_le_bayesRisk_comp.

theorem ProbabilityTheory.blackwellDominates_of_isGarblingOf {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] [m𝓧' : MeasurableSpace 𝓧'] {P : Kernel Θ 𝓧} {P' : Kernel Θ 𝓧'} (h : P'.IsGarblingOf P) : P.BlackwellDominates P'

Easy direction, bundled. A garbling of P is Blackwell-dominated by P.

The garbling polytope (finite case)

Over finite spaces, the Markov garblings {η ∘ₖ P | η Markov} of P, encoded by their singleton masses as vectors in Θ → 𝓧' → ℝ, form a compact convex polytope garblingSet P. It is the linear image of the product of standard simplices — the stochastic matrices η — under garblingMap P. This is the geometric substrate for the Blackwell–Sherman–Stein converse: if encode P' lies outside the polytope, a separating functional realizes a decision problem on which P' is strictly worse than P.

theorem ProbabilityTheory.isGarblingOf_of_bayesRisk_uniform_le {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] [m𝓧' : MeasurableSpace 𝓧'] [Fintype Θ] [Fintype 𝓧] [Fintype 𝓧'] [Nonempty Θ] [MeasurableSingletonClass Θ] [MeasurableSingletonClass 𝓧] [MeasurableSingletonClass 𝓧'] {P : Kernel Θ 𝓧} {P' : Kernel Θ 𝓧'} [IsMarkovKernel P] [IsMarkovKernel P'] (h : ∀ (ℓ : Θ → 𝓧' → ENNReal), (∀ (θ : Θ) (x' : 𝓧'), ℓ θ x' ≠ ⊤) → bayesRisk ℓ P ((↑(Fintype.card Θ))⁻¹ • MeasureTheory.Measure.count) ≤ bayesRisk ℓ P' ((↑(Fintype.card Θ))⁻¹ • MeasureTheory.Measure.count)) : P'.IsGarblingOf P

Blackwell–Sherman–Stein converse, minimal-hypothesis form. Same conclusion as isGarblingOf_of_blackwellDominates, but the risk-comparison hypothesis is required only for losses that are everywhere finite (ℓ θ x' ≠ ⊤) and only at the uniform prior. The proof body constructs exactly such a loss, so this weakened form is enough to conclude that P' is a garbling of P. Downstream users (e.g. Van Rooy's decision-theoretic converse transported through the utility–loss duality) supply only finite-valued losses.

theorem ProbabilityTheory.isGarblingOf_of_blackwellDominates {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] [m𝓧' : MeasurableSpace 𝓧'] [Fintype Θ] [Fintype 𝓧] [Fintype 𝓧'] [Nonempty Θ] [MeasurableSingletonClass Θ] [MeasurableSingletonClass 𝓧] [MeasurableSingletonClass 𝓧'] {P : Kernel Θ 𝓧} {P' : Kernel Θ 𝓧'} [IsMarkovKernel P] [IsMarkovKernel P'] (h : P.BlackwellDominates P') : P'.IsGarblingOf P

Blackwell–Sherman–Stein converse (finite case). If P Blackwell-dominates P' (attains a Bayes risk no larger than P' for every decision problem and prior), then P' is a garbling of P.

Stated for finite parameter and sample spaces, with both experiments Markov kernels. All four hypotheses are essential:

• The converse is false for general measurable spaces — this is the finite Blackwell equivalence ([Bla53]); the standard-Borel version additionally requires the experiments to be dominated.
• [Nonempty Θ] is necessary: with Θ empty every Bayes risk is 0, so the hypothesis holds vacuously, yet a Markov garbling η : Kernel 𝓧 𝓧' need not exist when 𝓧 is nonempty and 𝓧' is empty. (Nonempty Θ together with [IsMarkovKernel P'] also forces 𝓧' nonempty.)
• [IsMarkovKernel P] is necessary: a defective P can attain low risk without being informative. E.g. the zero kernel P = 0 has bayesRisk ℓ 0 π = 0 for every loss (the least possible value), so it dominates every P', yet η ∘ₖ 0 = 0 forces P' = 0.
• [IsMarkovKernel P'] is necessary: an over-massed P' inflates every risk. E.g. over a one-point sample space with P' = 2 • P one has bayesRisk ℓ P' π = 2 • bayesRisk ℓ P π ≥ bayesRisk ℓ P π for every loss, yet P' (mass 2) is not η ∘ₖ P for any Markov η.

The quantification over all decision problems is likewise essential: dominance for a single one does not force garbling.

The proof factors through isGarblingOf_of_bayesRisk_uniform_le: the internal separating loss is finite-valued, so the full universal quantification is stronger than needed.

theorem ProbabilityTheory.isGarblingOf_iff_blackwellDominates {Θ : Type u_1} {𝓧 : Type u_2} {𝓧' : Type u} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] [m𝓧' : MeasurableSpace 𝓧'] [Fintype Θ] [Fintype 𝓧] [Fintype 𝓧'] [Nonempty Θ] [MeasurableSingletonClass Θ] [MeasurableSingletonClass 𝓧] [MeasurableSingletonClass 𝓧'] {P : Kernel Θ 𝓧} {P' : Kernel Θ 𝓧'} [IsMarkovKernel P] [IsMarkovKernel P'] : P'.IsGarblingOf P ↔ P.BlackwellDominates P'

[Bla53] (finite case). P is at least as informative as P' (P' is a garbling of P) iff P Blackwell-dominates P' (no greater Bayes risk across every decision problem). The forward direction (blackwellDominates_of_isGarblingOf) holds for arbitrary spaces; the reverse (isGarblingOf_of_blackwellDominates) needs finiteness, nonempty Θ, and that both experiments are Markov kernels.

Deterministic experiments: partitions as kernels

A deterministic classifier f : Θ → 𝓧 is the experiment Kernel.deterministic f hf — the partition of Θ into the fibers of f, viewed as an error-free observation. Coarsening the partition (post-composing the classifier) is a deterministic garbling, so a finer partition Blackwell-dominates every coarsening. This is the kernel-level form of the fact that partition-refinement monotonicity of question value ([vR03a] §4.1, formalized ℚ-valued as Core.DecisionTheory.DecisionProblem.questionUtility_mono_of_refines) is a special case of [Bla53].

theorem ProbabilityTheory.Kernel.deterministic_comp_isGarblingOf_deterministic {Θ : Type u_1} {𝓧 : Type u_2} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] {𝓨 : Type u_3} [MeasurableSpace 𝓨] {f : Θ → 𝓧} {g : 𝓧 → 𝓨} (hf : Measurable f) (hg : Measurable g) : (deterministic (g ∘ f) ⋯).IsGarblingOf (deterministic f hf)

A coarsened classifier is a garbling of the classifier it factors through: the partition of g ∘ f is obtained from the partition of f by the deterministic post-processing g.

theorem ProbabilityTheory.bayesRisk_deterministic_le_deterministic_comp {Θ : Type u_1} {𝓧' : Type u} [mΘ : MeasurableSpace Θ] [m𝓧' : MeasurableSpace 𝓧'] {𝓨 : Type u} [MeasurableSpace 𝓨] {𝓨' : Type u} [MeasurableSpace 𝓨'] {f : Θ → 𝓧'} {g : 𝓧' → 𝓨} (hf : Measurable f) (hg : Measurable g) (ℓ : Θ → 𝓨' → ENNReal) (π : MeasureTheory.Measure Θ) : bayesRisk ℓ (Kernel.deterministic f hf) π ≤ bayesRisk ℓ (Kernel.deterministic (g ∘ f) ⋯) π

A finer partition is worth at least as much as any coarsening, in every decision problem: the Bayes risk of the experiment "observe f θ" is at most that of "observe g (f θ)". The kernel-level [Bla53] fact behind [vR03a]'s §4.1 question-utility monotonicity.

theorem ProbabilityTheory.Kernel.deterministic_isGarblingOf_deterministic_iff {Θ : Type u_1} {𝓧 : Type u_2} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] {𝓨 : Type u_3} [MeasurableSpace 𝓨] [Countable 𝓧] [MeasurableSingletonClass 𝓧] [MeasurableSingletonClass 𝓨] [Nonempty 𝓨] {f : Θ → 𝓧} {g : Θ → 𝓨} (hf : Measurable f) (hg : Measurable g) : (deterministic g hg).IsGarblingOf (deterministic f hf) ↔ ∃ (ψ : 𝓧 → 𝓨), g = ψ ∘ f

Between deterministic experiments the Blackwell order is functional factoring: deterministic g is a garbling of deterministic f iff g factors through f. The mixing kernel of any garbling of a deterministic experiment is forced to be Dirac on the range of f, so randomized post-processing buys nothing — the partition of g must genuinely coarsen the partition of f.

theorem ProbabilityTheory.bayesRisk_deterministic {Θ : Type u_1} {𝓧 : Type u_2} [mΘ : MeasurableSpace Θ] [m𝓧 : MeasurableSpace 𝓧] [Fintype Θ] [Fintype 𝓧] [DecidableEq 𝓧] [MeasurableSingletonClass Θ] [MeasurableSingletonClass 𝓧] {𝓨 : Type u} [MeasurableSpace 𝓨] [Fintype 𝓨] [Nonempty 𝓨] [MeasurableSingletonClass 𝓨] {f : Θ → 𝓧} (hf : Measurable f) (ℓ : Θ → 𝓨 → ENNReal) (π : MeasureTheory.Measure Θ) [MeasureTheory.IsFiniteMeasure π] : bayesRisk ℓ (Kernel.deterministic f hf) π = ∑ x : 𝓧, ⨅ (y : 𝓨), ∑ θ : Θ with f θ = x, π {θ} * ℓ θ y

Bayes risk of a deterministic experiment (finite case): observing the exact cell of θ under f, the optimal estimator picks the best action per cell, so the Bayes risk is the sum over cells of the minimal conditional expected loss. The utility-scale reading — risk = bound minus partition value — is Core.Probability.Decision.Duality.