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. On the utility scale, Core.Probability.Decision.ValueOfInformation reads the data-processing direction as the statement that garbling an experiment never raises its value of information, and reads the converse for deterministic experiments as a comparison of the value of observing classifiers.

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 (StdSimplex.compactSpace, 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 when a Markov kernel η post-processes P into P', so that P' = η ∘ₖ P and 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' when, for every decision problem (an action space 𝓨 with a loss ℓ) and every prior π, the Bayes risk under P is at most that under P'.

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' π

If P' is a garbling of P, the Bayes risk under P is at most that under P' in every decision problem.

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'

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. If encode P' lies outside the polytope, a separating functional gives a decision problem on which P' is strictly worse than P, which proves the converse.

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

If P has Bayes risk at most that of P' under the uniform prior for every everywhere-finite loss, then P' is a garbling of P.

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

On finite spaces with Θ nonempty, if P Blackwell-dominates P' and both are Markov kernels, then P' is a garbling of P.

Each hypothesis is needed. With Θ empty every Bayes risk is 0, yet no Markov kernel maps a nonempty 𝓧 to an empty 𝓧'. The zero kernel has Bayes risk 0 for every loss and so dominates every P', yet η ∘ₖ 0 = 0. Over a one-point sample space P' = 2 • P has twice the Bayes risk of P for every loss, yet is no Markov garbling of P. Dominance in a single decision problem does not force garbling either.

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'

On finite spaces with Θ nonempty and Markov P and P', P' is a garbling of P exactly when P Blackwell-dominates P'.

Deterministic experiments: partitions as kernels

A deterministic classifier f : Θ → 𝓧 is the experiment Kernel.deterministic f hf, an error-free observation of the cell of θ in the partition of Θ into the fibers of f. Between deterministic experiments the garbling order is functional factoring.

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

deterministic g is a garbling of deterministic f exactly when g factors through f; randomized post-processing gains nothing between deterministic experiments.