Hellinger distance on a finite type

The Bhattacharyya coefficient ∑ a, √(μ {a} · ν {a}) of two measures on a finite type, the squared Hellinger distance 1 - BC, and the Hellinger distance √(1 - BC). For probability measures the coefficient lies in [0, 1], so the Hellinger distance is bounded by 1 where the Kullback–Leibler divergence may be infinite. Mathlib has no Hellinger distance; [UPSTREAM] candidate for Mathlib/InformationTheory/.

noncomputable def InformationTheory.bhattacharyyaCoeff {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ ν : MeasureTheory.Measure α) : ℝ

The Bhattacharyya coefficient ∑ a, √(μ {a} · ν {a}).

Equations

• InformationTheory.bhattacharyyaCoeff μ ν = ∑ a : α, √(μ.real {a} * ν.real {a})

noncomputable def InformationTheory.hellingerDistSq {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ ν : MeasureTheory.Measure α) : ℝ

The squared Hellinger distance 1 - BC(μ, ν).

Equations

• InformationTheory.hellingerDistSq μ ν = 1 - InformationTheory.bhattacharyyaCoeff μ ν

noncomputable def InformationTheory.hellingerDist {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ ν : MeasureTheory.Measure α) : ℝ

The Hellinger distance √(1 - BC(μ, ν)).

Equations

• InformationTheory.hellingerDist μ ν = √(InformationTheory.hellingerDistSq μ ν)

theorem InformationTheory.bhattacharyyaCoeff_nonneg {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ ν : MeasureTheory.Measure α) : 0 ≤ bhattacharyyaCoeff μ ν

theorem InformationTheory.hellingerDistSq_le_one {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ ν : MeasureTheory.Measure α) : hellingerDistSq μ ν ≤ 1

theorem InformationTheory.hellingerDist_le_one {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ ν : MeasureTheory.Measure α) : hellingerDist μ ν ≤ 1

theorem InformationTheory.bhattacharyyaCoeff_le_one {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ ν : MeasureTheory.Measure α) [MeasurableSingletonClass α] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : bhattacharyyaCoeff μ ν ≤ 1

For probability measures the Bhattacharyya coefficient is at most 1, by the arithmetic–geometric mean inequality on each atom.

theorem InformationTheory.hellingerDistSq_nonneg {α : Type u_1} [MeasurableSpace α] [Fintype α] (μ ν : MeasureTheory.Measure α) [MeasurableSingletonClass α] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : 0 ≤ hellingerDistSq μ ν

theorem InformationTheory.bhattacharyyaCoeff_dirac_left {α : Type u_1} [MeasurableSpace α] [Fintype α] (ν : MeasureTheory.Measure α) [MeasurableSingletonClass α] (a : α) : bhattacharyyaCoeff (MeasureTheory.Measure.dirac a) ν = √(ν.real {a})

The Bhattacharyya coefficient against a Dirac mass is the square root of the other measure's mass at the atom.

theorem InformationTheory.hellingerDist_dirac_left {α : Type u_1} [MeasurableSpace α] [Fintype α] (ν : MeasureTheory.Measure α) [MeasurableSingletonClass α] (a : α) : hellingerDist (MeasureTheory.Measure.dirac a) ν = √(1 - √(ν.real {a}))

The Hellinger distance from a Dirac mass is determined by the other measure's mass at the atom: 1 where that mass vanishes.