E-variable divergences #
We define analogues of the Rényi and Chernoff divergences for e-variables that share the same properties as the classical divergences. In particular, they satisfy a data processing inequality.
Main definitions #
erenyiDiv α S T: the e-Rényi divergence of orderαbetween two sets of measuresSandT.echernoffDiv S T: the e-Chernoff divergence between two sets of measuresSandT.
Main statements #
erenyiDiv_comp_le: data processing inequality for the e-Rényi divergence.echernoffDiv_comp_le: data processing inequality for the e-Chernoff divergence.erenyiDiv_prod: e-Rényi divergence of product sets of measures is the sum of the e-Rényi divergences.echernoffDiv_prod_le: e-Chernoff divergence of product sets of measures is less than the sum of the e-Chernoff divergences.
noncomputable def
ProbabilityTheory.erenyiDiv
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
(α : ENNReal)
(S T : Set (MeasureTheory.Measure 𝓧))
:
The e-Rényi divergence between two sets of measures.
Note that the two integrals are non-negative, so the application of EReal.toENNReal does not
truncate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.erenyiDiv_eq_sInf
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{S T : Set (MeasureTheory.Measure 𝓧)}
{α : ENNReal}
:
erenyiDiv α S T = (1 - α)⁻¹ * sInf
{y : ENNReal | ∃ (R : MeasureTheory.Measure 𝓧),
MeasureTheory.IsProbabilityMeasure R ∧ y = α * (maxUtility R S logUtility).toENNReal + (1 - α) * (maxUtility R T logUtility).toENNReal}
theorem
ProbabilityTheory.erenyiDiv_empty_left
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{α : ENNReal}
{T : Set (MeasureTheory.Measure 𝓧)}
(hα : α ≠ 0)
:
theorem
ProbabilityTheory.erenyiDiv_empty_right
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{α : ENNReal}
{S : Set (MeasureTheory.Measure 𝓧)}
(hα : α < 1)
:
@[simp]
noncomputable def
ProbabilityTheory.echernoffDiv
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
(S T : Set (MeasureTheory.Measure 𝓧))
:
The e-Chernoff divergence between two sets of measures.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ProbabilityTheory.echernoffDiv_eq_sInf
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{S T : Set (MeasureTheory.Measure 𝓧)}
:
echernoffDiv S T = sInf
{y : ENNReal | ∃ (R : MeasureTheory.Measure 𝓧),
MeasureTheory.IsProbabilityMeasure R ∧ y = max (maxUtility R S logUtility).toENNReal (maxUtility R T logUtility).toENNReal}
theorem
ProbabilityTheory.erenyiDiv_anti
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{α : ENNReal}
{S₁ S₂ T₁ T₂ : Set (MeasureTheory.Measure 𝓧)}
(hS : S₁ ⊆ S₂)
(hT : T₁ ⊆ T₂)
:
theorem
ProbabilityTheory.echernoffDiv_anti
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{S₁ S₂ T₁ T₂ : Set (MeasureTheory.Measure 𝓧)}
(hS : S₁ ⊆ S₂)
(hT : T₁ ⊆ T₂)
:
theorem
ProbabilityTheory.erenyiDiv_comp_le
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{S T : Set (MeasureTheory.Measure 𝓧)}
{α : ENNReal}
(κ : Kernel 𝓧 𝓨)
[IsMarkovKernel κ]
:
Data processing inequality for the e-Rényi divergence with a Markov kernel.
theorem
ProbabilityTheory.erenyiDiv_map_le
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{S T : Set (MeasureTheory.Measure 𝓧)}
{α : ENNReal}
{f : 𝓧 → 𝓨}
(hf : Measurable f)
:
erenyiDiv α {x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ S, MeasureTheory.Measure.map f μ = x}
{x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ T, MeasureTheory.Measure.map f μ = x} ≤ erenyiDiv α S T
Data processing inequality for the e-Rényi divergence with a measurable function.
theorem
ProbabilityTheory.echernoffDiv_comp_le
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{S T : Set (MeasureTheory.Measure 𝓧)}
(κ : Kernel 𝓧 𝓨)
[IsMarkovKernel κ]
:
echernoffDiv {x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ S, μ.bind ⇑κ = x}
{x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ T, μ.bind ⇑κ = x} ≤ echernoffDiv S T
Data processing inequality for the e-Chernoff divergence with a Markov kernel.
theorem
ProbabilityTheory.echernoffDiv_map_le
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{S T : Set (MeasureTheory.Measure 𝓧)}
{f : 𝓧 → 𝓨}
(hf : Measurable f)
:
echernoffDiv {x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ S, MeasureTheory.Measure.map f μ = x}
{x : MeasureTheory.Measure 𝓨 | ∃ μ ∈ T, MeasureTheory.Measure.map f μ = x} ≤ echernoffDiv S T
Data processing inequality for the e-Chernoff divergence with a measurable function.
theorem
ProbabilityTheory.erenyiDiv_add_eq_sInf
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{α : ENNReal}
(S₁ S₂ : Set (MeasureTheory.Measure 𝓧))
(T₁ T₂ : Set (MeasureTheory.Measure 𝓨))
:
(1 - α)⁻¹ * sInf
{y : ENNReal | ∃ (R₁ : MeasureTheory.Measure 𝓧) (R₂ : MeasureTheory.Measure 𝓨),
MeasureTheory.IsProbabilityMeasure R₁ ∧ MeasureTheory.IsProbabilityMeasure R₂ ∧ y = α * (maxUtility R₁ S₁ logUtility + maxUtility R₂ T₁ logUtility).toENNReal + (1 - α) * (maxUtility R₁ S₂ logUtility + maxUtility R₂ T₂ logUtility).toENNReal} = erenyiDiv α S₁ S₂ + erenyiDiv α T₁ T₂
theorem
ProbabilityTheory.erenyiDiv_prod_le
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{α : ENNReal}
{S₁ S₂ : Set (MeasureTheory.Measure 𝓧)}
{T₁ T₂ : Set (MeasureTheory.Measure 𝓨)}
(hS₁ : ∀ μ ∈ S₁, MeasureTheory.IsFiniteMeasure μ)
(hS₂ : ∀ μ ∈ S₂, MeasureTheory.IsFiniteMeasure μ)
(hT₁ : ∀ μ ∈ T₁, MeasureTheory.IsFiniteMeasure μ)
(hT₂ : ∀ μ ∈ T₂, MeasureTheory.IsFiniteMeasure μ)
:
erenyiDiv α (Function.uncurry MeasureTheory.Measure.prod '' S₁ ×ˢ T₁)
(Function.uncurry MeasureTheory.Measure.prod '' S₂ ×ˢ T₂) ≤ erenyiDiv α S₁ S₂ + erenyiDiv α T₁ T₂
theorem
ProbabilityTheory.erenyiDiv_prod
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{α : ENNReal}
{S₁ S₂ : Set (MeasureTheory.Measure 𝓧)}
{T₁ T₂ : Set (MeasureTheory.Measure 𝓨)}
(hS₁ : ∀ μ ∈ S₁, MeasureTheory.IsFiniteMeasure μ)
(hS₂ : ∀ μ ∈ S₂, MeasureTheory.IsFiniteMeasure μ)
(hT₁ : ∀ μ ∈ T₁, MeasureTheory.IsFiniteMeasure μ)
(hT₂ : ∀ μ ∈ T₂, MeasureTheory.IsFiniteMeasure μ)
:
erenyiDiv α (Function.uncurry MeasureTheory.Measure.prod '' S₁ ×ˢ T₁)
(Function.uncurry MeasureTheory.Measure.prod '' S₂ ×ˢ T₂) = erenyiDiv α S₁ S₂ + erenyiDiv α T₁ T₂
theorem
ProbabilityTheory.echernoffDiv_prod_le
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{S₁ S₂ : Set (MeasureTheory.Measure 𝓧)}
{T₁ T₂ : Set (MeasureTheory.Measure 𝓨)}
(hS₁ : ∀ μ ∈ S₁, MeasureTheory.IsFiniteMeasure μ)
(hS₂ : ∀ μ ∈ S₂, MeasureTheory.IsFiniteMeasure μ)
(hT₁ : ∀ μ ∈ T₁, MeasureTheory.IsFiniteMeasure μ)
(hT₂ : ∀ μ ∈ T₂, MeasureTheory.IsFiniteMeasure μ)
:
echernoffDiv (Function.uncurry MeasureTheory.Measure.prod '' S₁ ×ˢ T₁)
(Function.uncurry MeasureTheory.Measure.prod '' S₂ ×ˢ T₂) ≤ echernoffDiv S₁ S₂ + echernoffDiv T₁ T₂
theorem
ProbabilityTheory.erenyiDiv_of_involutive_aux
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{S T : Set (MeasureTheory.Measure 𝓧)}
{φ : 𝓧 → 𝓧}
(hφ : Measurable φ)
(hφ_inv : φ ∘ φ = id)
(hφST : {x : MeasureTheory.Measure 𝓧 | ∃ μ ∈ S, MeasureTheory.Measure.map φ μ = x} = T)
:
erenyiDiv 2⁻¹ S T = 2 * ⨅ (R : MeasureTheory.Measure 𝓧),
⨅ (_ : MeasureTheory.IsProbabilityMeasure R),
⨅ (_ : MeasureTheory.Measure.map φ R = R),
2⁻¹ * (maxUtility R S logUtility).toENNReal + 2⁻¹ * (maxUtility R T logUtility).toENNReal
theorem
ProbabilityTheory.erenyiDiv_of_involutive
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{S T : Set (MeasureTheory.Measure 𝓧)}
{φ : 𝓧 → 𝓧}
(hφ : Measurable φ)
(hφ_inv : φ ∘ φ = id)
(hφST : {x : MeasureTheory.Measure 𝓧 | ∃ μ ∈ S, MeasureTheory.Measure.map φ μ = x} = T)
:
erenyiDiv 2⁻¹ S T = 2 * ⨅ (R : MeasureTheory.Measure 𝓧),
⨅ (_ : MeasureTheory.IsProbabilityMeasure R),
⨅ (_ : MeasureTheory.Measure.map φ R = R), (maxUtility R S logUtility).toENNReal
theorem
ProbabilityTheory.echernoffDiv_of_involutive_aux
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{S T : Set (MeasureTheory.Measure 𝓧)}
{φ : 𝓧 → 𝓧}
(hφ : Measurable φ)
(hφ_inv : φ ∘ φ = id)
(hφST : {x : MeasureTheory.Measure 𝓧 | ∃ μ ∈ S, MeasureTheory.Measure.map φ μ = x} = T)
:
echernoffDiv S T = ⨅ (R : MeasureTheory.Measure 𝓧),
⨅ (_ : MeasureTheory.IsProbabilityMeasure R),
⨅ (_ : MeasureTheory.Measure.map φ R = R),
max (maxUtility R S logUtility).toENNReal (maxUtility R T logUtility).toENNReal
theorem
ProbabilityTheory.echernoffDiv_of_involutive
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{S T : Set (MeasureTheory.Measure 𝓧)}
{φ : 𝓧 → 𝓧}
(hφ : Measurable φ)
(hφ_inv : φ ∘ φ = id)
(hφST : {x : MeasureTheory.Measure 𝓧 | ∃ μ ∈ S, MeasureTheory.Measure.map φ μ = x} = T)
:
echernoffDiv S T = ⨅ (R : MeasureTheory.Measure 𝓧),
⨅ (_ : MeasureTheory.IsProbabilityMeasure R),
⨅ (_ : MeasureTheory.Measure.map φ R = R), (maxUtility R S logUtility).toENNReal
theorem
ProbabilityTheory.erenyiDiv_eq_two_mul_echernoffDiv_of_involutive
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{S T : Set (MeasureTheory.Measure 𝓧)}
{φ : 𝓧 → 𝓧}
(hφ : Measurable φ)
(hφ_inv : φ ∘ φ = id)
(hφST : {x : MeasureTheory.Measure 𝓧 | ∃ μ ∈ S, MeasureTheory.Measure.map φ μ = x} = T)
: