Lower bound on e-Rényi and e-Chernoff divergences #
This file contains proofs of lower bounds on the e-Rényi and e-Chernoff divergences between sets of probability measures with bounded expectations.
Results #
erenyiDiv_bounded_eq_erenyiDiv_bernoulli: The e-Rényi divergence between sets of probability measures on the unit interval with bounded expectations is equal to the e-Rényi divergence between corresponding sets of Bernoulli distributions.erenyiDiv_bounded: A closed-form expression for the e-Rényi divergence between sets of probability measures on the unit interval with bounded expectations.echernoffDiv_bounded: A closed-form expression for the e-Chernoff divergence between sets of probability measures on the unit interval with bounded expectations.erenyiDiv_ge_of_separated: A lower bound on the e-Rényi divergence between sets of probability measures with bounded expectations w.r.t. a measurable function.echernoffDiv_ge_of_separated: A lower bound on the e-Chernoff divergence between sets of probability measures with bounded expectations w.r.t. a measurable function.
theorem
ProbabilityTheory.erenyiDiv_bounded_eq_erenyiDiv_bernoulli
{α : ENNReal}
{a b : ℝ}
:
erenyiDiv α
{μ : MeasureTheory.Measure ↑unitInterval | MeasureTheory.IsProbabilityMeasure μ ∧ ∫ (x : ↑unitInterval), ↑x ∂μ ≤ a}
{μ : MeasureTheory.Measure ↑unitInterval | MeasureTheory.IsProbabilityMeasure μ ∧ b ≤ ∫ (x : ↑unitInterval), ↑x ∂μ} = erenyiDiv α {μ : MeasureTheory.Measure ↑{0, 1} | MeasureTheory.IsProbabilityMeasure μ ∧ ∫ (x : ↑{0, 1}), ↑x ∂μ ≤ a}
{μ : MeasureTheory.Measure ↑{0, 1} | MeasureTheory.IsProbabilityMeasure μ ∧ b ≤ ∫ (x : ↑{0, 1}), ↑x ∂μ}
theorem
ProbabilityTheory.erenyiDiv_bounded
{δ : ℝ}
(hδ_pos : 0 < δ)
(hδ : δ ≤ 2⁻¹)
:
erenyiDiv 2⁻¹
{μ : MeasureTheory.Measure ↑unitInterval | MeasureTheory.IsProbabilityMeasure μ ∧ ∫ (x : ↑unitInterval), ↑x ∂μ ≤ δ}
{μ : MeasureTheory.Measure ↑unitInterval | MeasureTheory.IsProbabilityMeasure μ ∧ 1 - δ ≤ ∫ (x : ↑unitInterval), ↑x ∂μ} = ENNReal.ofReal (Real.log (1 / (4 * δ * (1 - δ))))
theorem
ProbabilityTheory.echernoffDiv_bounded
{δ : ℝ}
(hδ_pos : 0 < δ)
(hδ : δ ≤ 2⁻¹)
:
echernoffDiv
{μ : MeasureTheory.Measure ↑unitInterval | MeasureTheory.IsProbabilityMeasure μ ∧ ∫ (x : ↑unitInterval), ↑x ∂μ ≤ δ}
{μ : MeasureTheory.Measure ↑unitInterval | MeasureTheory.IsProbabilityMeasure μ ∧ 1 - δ ≤ ∫ (x : ↑unitInterval), ↑x ∂μ} = 2⁻¹ * ENNReal.ofReal (Real.log (1 / (4 * δ * (1 - δ))))
theorem
ProbabilityTheory.erenyiDiv_ge_of_separated
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{S T : Set (MeasureTheory.Measure 𝓧)}
{f : 𝓧 → ↑unitInterval}
(hf : Measurable f)
(hS : ∀ μ ∈ S, MeasureTheory.IsProbabilityMeasure μ)
(hT : ∀ μ ∈ T, MeasureTheory.IsProbabilityMeasure μ)
{δ : ℝ}
(hδ_pos : 0 < δ)
(hδ : δ ≤ 2⁻¹)
(hSf : ∀ μ ∈ S, ∫ (ω : 𝓧), ↑(f ω) ∂μ ≤ δ)
(hTf : ∀ ν ∈ T, 1 - δ ≤ ∫ (ω : 𝓧), ↑(f ω) ∂ν)
:
theorem
ProbabilityTheory.echernoffDiv_ge_of_separated
{𝓧 : Type u_1}
{m𝓧 : MeasurableSpace 𝓧}
{S T : Set (MeasureTheory.Measure 𝓧)}
{f : 𝓧 → ↑unitInterval}
(hf : Measurable f)
(hS : ∀ μ ∈ S, MeasureTheory.IsProbabilityMeasure μ)
(hT : ∀ μ ∈ T, MeasureTheory.IsProbabilityMeasure μ)
{δ : ℝ}
(hδ_pos : 0 < δ)
(hδ : δ ≤ 2⁻¹)
(hSf : ∀ μ ∈ S, ∫ (ω : 𝓧), ↑(f ω) ∂μ ≤ δ)
(hTf : ∀ ν ∈ T, 1 - δ ≤ ∫ (ω : 𝓧), ↑(f ω) ∂ν)
: