Boundary inequality: 2 q² ≤ -log(1 - q) on [0, 1)

The two variants two_sq_le_neg_log_one_sub and two_sq_le_neg_log handle the p = 0 and p = 1 boundary cases of the binary Pinsker theorem. Proved via monotonicity of h(q) = -log(1-q) - 2 q² on [0, 1); the derivative 1/(1-q) - 4q = (2q-1)²/(1-q) ≥ 0.

theorem InformationTheory.two_sq_le_neg_log_one_sub (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q < 1) : 2 * q ^ 2 ≤ -Real.log (1 - q)

2 q² ≤ -log(1 - q) for q ∈ [0, 1).

theorem InformationTheory.two_sq_le_neg_log (q : ℝ) (hq₀ : 0 < q) (hq₁ : q ≤ 1) : 2 * (1 - q) ^ 2 ≤ -Real.log q

2 (1 - q)² ≤ -log q for q ∈ (0, 1]. Substitute r = 1 - q into the previous.