Chernoff divergence

Main definitions

• chernoffDiv

Main statements

• fooBar_unique

noncomputable def ProbabilityTheory.chernoffDiv {α : Type u_1} {mα : MeasurableSpace α} (a : ℝ) (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : EReal

Chernoff divergence of order a between two measures μ, ν. This is the infimum over probability measures ξ of the maximum of the Rényi divergences of order a from ξ to μ and from ξ to ν.

Equations

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

theorem ProbabilityTheory.chernoffDiv_one {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : ProbabilityTheory.chernoffDiv 1 μ ν = ⨅ (ξ : MeasureTheory.Measure α), ⨅ (_ : MeasureTheory.IsProbabilityMeasure ξ), max (ProbabilityTheory.kl ξ μ) (ProbabilityTheory.kl ξ ν)