Binary Pinsker inequality

2 (p − q)² ≤ klBin p q for p ∈ [0, 1] and q ∈ (0, 1). Case-splits on p = 0, p = 1, and p ∈ (0, 1), with the middle case further reducing to monotonicity of g on the appropriate half-interval around p.

theorem InformationTheory.binary_pinsker (p q : ℝ) (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) (hq₀ : 0 < q) (hq₁ : q < 1) : 2 * (p - q) ^ 2 ≤ klBin p q

Binary Pinsker inequality. 2 (p − q)² ≤ klBin p q for p ∈ [0, 1], q ∈ (0, 1). Sharp constant 2.