Monotonicity of g(q) = klBin p q − 2 (p − q)² on (0, p] and [p, 1)

The derivative factor (1 − 2q)² / (q (1 − q)) is nonnegative on (0, 1), so the sign of the derivative of g reduces to sign(q − p). This makes g antitone on (0, p] and monotone on [p, 1). These are the two intervals that the binary Pinsker proof reduces to via case split on p ≤ q vs q ≤ p.

theorem InformationTheory.deriv_factor_nonneg (q : ℝ) (hq₀ : 0 < q) (hq₁ : q < 1) : 0 ≤ (1 - 2 * q) ^ 2 / (q * (1 - q))

The derivative factor (1 − 2q)² / (q (1 − q)) is nonnegative on (0, 1).

theorem InformationTheory.deriv_g_nonneg_of_ge (p q : ℝ) (hpq : p ≤ q) (hq₀ : 0 < q) (hq₁ : q < 1) : 0 ≤ (q - p) * (1 - 2 * q) ^ 2 / (q * (1 - q))

On [p, 1): derivative of g is nonnegative.

theorem InformationTheory.deriv_g_nonpos_of_le (p q : ℝ) (hqp : q ≤ p) (hq₀ : 0 < q) (hq₁ : q < 1) : (q - p) * (1 - 2 * q) ^ 2 / (q * (1 - q)) ≤ 0

On (0, p]: derivative of g is nonpositive.

theorem InformationTheory.monotoneOn_g (p : ℝ) (hp₀ : 0 < p) (hp₁ : p < 1) : MonotoneOn (fun (q : ℝ) => klBin p q - 2 * (p - q) ^ 2) (Set.Ico p 1)

g(q) = klBin p q − 2 (p − q)² is monotone on [p, 1).

theorem InformationTheory.antitoneOn_g (p : ℝ) (hp₀ : 0 < p) (hp₁ : p < 1) : AntitoneOn (fun (q : ℝ) => klBin p q - 2 * (p - q) ^ 2) (Set.Ioc 0 p)

g(q) = klBin p q − 2 (p − q)² is antitone on (0, p].