Risk increase (or statistical information) #
A way to quantify the information obtained by an experiment is to look at the increase in risk that results from discarding the observation of that experiment. We call that quantity the risk increase. It was called information by DeGroot in [DeG62], but we opt for a more descriptive name to avoid confusion with other notions of information in statistics and information theory. See also [DKR18] for properties of the risk increase and relations to statistical divergences.
Main definitions #
riskIncrease ℓ P π: the increase in risk that results from discarding the observation in a Bayesian estimation problem, equal tobayesRisk ℓ (Kernel.discard 𝓧 ∘ₖ P) π - bayesRisk ℓ P π.
Main statements #
riskIncrease_comp_le: the data-processing inequality for the risk increase, which states that the risk increase cannot be increased by post-processing the observation (composing the kernelPwith a Markov kernel):riskIncrease ℓ (η ∘ₖ P) π ≤ riskIncrease ℓ P π.riskIncrease_map_le: version of the data-processing inequality for a measurable function instead of a Markov kernel.riskIncrease ℓ (P.map f) π ≤ riskIncrease ℓ P π.
noncomputable def
ProbabilityTheory.riskIncrease
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
(ℓ : Θ → 𝓨 → ENNReal)
(P : Kernel Θ 𝓧)
(π : MeasureTheory.Measure Θ)
:
The increase in risk that results from discarding the observation in a Bayesian estimation problem.
Equations
Instances For
theorem
ProbabilityTheory.riskIncrease_eq_iInf_sub'
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
{ℓ : Θ → 𝓨 → ENNReal}
[Nonempty 𝓨]
(hℓ : Measurable (Function.uncurry ℓ))
(P : Kernel Θ 𝓧)
(π : MeasureTheory.Measure Θ)
[MeasureTheory.SFinite π]
:
theorem
ProbabilityTheory.riskIncrease_eq_iInf_sub
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
{ℓ : Θ → 𝓨 → ENNReal}
(hℓ : Measurable (Function.uncurry ℓ))
(P : Kernel Θ 𝓧)
[IsMarkovKernel P]
(π : MeasureTheory.Measure Θ)
[MeasureTheory.SFinite π]
:
@[simp]
theorem
ProbabilityTheory.riskIncrease_of_isEmpty_of_isEmpty
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
{π : MeasureTheory.Measure Θ}
{P : Kernel Θ 𝓧}
{ℓ : Θ → 𝓨 → ENNReal}
[IsEmpty 𝓧]
[IsEmpty 𝓨]
:
@[simp]
theorem
ProbabilityTheory.riskIncrease_of_nonempty_of_isEmpty
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
{π : MeasureTheory.Measure Θ}
{P : Kernel Θ 𝓧}
{ℓ : Θ → 𝓨 → ENNReal}
[Nonempty 𝓧]
[IsEmpty 𝓨]
:
@[simp]
theorem
ProbabilityTheory.riskIncrease_zero_left
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
{π : MeasureTheory.Measure Θ}
{ℓ : Θ → 𝓨 → ENNReal}
[Nonempty 𝓨]
:
@[simp]
theorem
ProbabilityTheory.riskIncrease_zero_right
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
{P : Kernel Θ 𝓧}
{ℓ : Θ → 𝓨 → ENNReal}
[Nonempty 𝓨]
:
@[simp]
theorem
ProbabilityTheory.riskIncrease_const
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
{π : MeasureTheory.Measure Θ}
{ℓ : Θ → 𝓨 → ENNReal}
(hℓ : Measurable (Function.uncurry ℓ))
[MeasureTheory.SFinite π]
{μ : MeasureTheory.Measure 𝓧}
[MeasureTheory.IsProbabilityMeasure μ]
:
theorem
ProbabilityTheory.riskIncrease_le_iInf'
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
{π : MeasureTheory.Measure Θ}
{P : Kernel Θ 𝓧}
{ℓ : Θ → 𝓨 → ENNReal}
[Nonempty 𝓨]
(hℓ : Measurable (Function.uncurry ℓ))
[MeasureTheory.SFinite π]
:
theorem
ProbabilityTheory.riskIncrease_le_iInf
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
{π : MeasureTheory.Measure Θ}
{P : Kernel Θ 𝓧}
{ℓ : Θ → 𝓨 → ENNReal}
(hℓ : Measurable (Function.uncurry ℓ))
[IsMarkovKernel P]
[MeasureTheory.SFinite π]
:
theorem
ProbabilityTheory.riskIncrease_lt_top'
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
{π : MeasureTheory.Measure Θ}
{P : Kernel Θ 𝓧}
{ℓ : Θ → 𝓨 → ENNReal}
[Nonempty 𝓨]
(hℓ : Measurable (Function.uncurry ℓ))
[MeasureTheory.IsFiniteMeasure π]
{y : 𝓨}
(h_finite : ∫⁻ (θ : Θ), (P θ) Set.univ * ℓ θ y ∂π ≠ ⊤)
:
theorem
ProbabilityTheory.riskIncrease_lt_top
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSpace 𝓨]
{π : MeasureTheory.Measure Θ}
{P : Kernel Θ 𝓧}
{ℓ : Θ → 𝓨 → ENNReal}
(hℓ : Measurable (Function.uncurry ℓ))
[IsMarkovKernel P]
[MeasureTheory.IsFiniteMeasure π]
{y : 𝓨}
(h_finite : ∫⁻ (θ : Θ), ℓ θ y ∂π ≠ ⊤)
:
theorem
ProbabilityTheory.riskIncrease_comp_le
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓧' : Type u_3}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓧' : MeasurableSpace 𝓧'}
[MeasurableSpace 𝓨]
(ℓ : Θ → 𝓨 → ENNReal)
(P : Kernel Θ 𝓧)
(π : MeasureTheory.Measure Θ)
(η : Kernel 𝓧 𝓧')
[IsMarkovKernel η]
:
Data processing inequality for the risk increase.
theorem
ProbabilityTheory.riskIncrease_map_le
{Θ : Type u_1}
{𝓧 : Type u_2}
{𝓧' : Type u_3}
{𝓨 : Type u_4}
{mΘ : MeasurableSpace Θ}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓧' : MeasurableSpace 𝓧'}
[MeasurableSpace 𝓨]
(ℓ : Θ → 𝓨 → ENNReal)
(P : Kernel Θ 𝓧)
(π : MeasureTheory.Measure Θ)
{f : 𝓧 → 𝓧'}
(hf : Measurable f)
:
Data processing inequality for the risk increase.