Derivatives of klBin and the auxiliary function g(q) = klBin p q − 2 (p − q)²

The derivative of klBin p q with respect to q is (q − p) / (q (1 − q)). The derivative of (p − q)² is −2 (p − q). Their difference gives the factored form (q − p) · (1 − 2q)² / (q (1 − q)), whose sign reduces to sign(q − p).

theorem InformationTheory.hasDerivAt_klBin_q (p q : ℝ) (hp₀ : 0 < p) (hp₁ : p < 1) (hq₀ : 0 < q) (hq₁ : q < 1) : HasDerivAt (fun (q : ℝ) => klBin p q) ((q - p) / (q * (1 - q))) q

Derivative of klBin p · at a point q ∈ (0, 1) with p ∈ (0, 1).

theorem InformationTheory.hasDerivAt_sub_sq (p q : ℝ) : HasDerivAt (fun (q : ℝ) => (p - q) ^ 2) (-2 * (p - q)) q

Derivative of (p − q)² with respect to q.

theorem InformationTheory.hasDerivAt_g (p q : ℝ) (hp₀ : 0 < p) (hp₁ : p < 1) (hq₀ : 0 < q) (hq₁ : q < 1) : HasDerivAt (fun (q : ℝ) => klBin p q - 2 * (p - q) ^ 2) ((q - p) * (1 - 2 * q) ^ 2 / (q * (1 - q))) q

Factored derivative identity. Derivative of g(q) := klBin(p, q) − 2 (p − q)² has the factored form (q − p) · (1 − 2q)² / (q · (1 − q)), reducing the sign of the derivative to sign(q − p).