The supporting line of x ↦ x * log x

The function x ↦ x * log x of Mathlib's Mathlib.Analysis.SpecialFunctions.Log.NegMulLog is strictly convex on the nonnegative reals. This file records the two estimates about it that the optimisation arguments over matrices and over measures use: the tangent line at a positive point lies below the graph at every nonnegative point, and the loss of the function at a point that gives up a small amount of its value is bounded by that same tangent line.

Main results

• Real.mul_log_sub_mul_log_ge: for 0 < a and 0 ≤ u, u * log u - a * log a ≥ (u - a) * (log a + 1).
• Real.sub_mul_log_le: for 0 ≤ t and t ≤ x / 2, (x - t) * log (x - t) - x * log x ≤ -t * (log x - log 2 + 1).
• TauCeti.sq_sqrt_sub_sqrt_le_mul_log_sub_mul_log_sub: for 0 < a and 0 ≤ u, the gap between the graph and the supporting line at a is at least (√u - √a) ^ 2.

The first estimate is the tangent line at a, whose slope log a + 1 is the derivative Real.deriv_mul_log of the function. It is stated for u = 0 as well, where the convention 0 * log 0 = 0 of Mathlib makes its left side -a * log a, so that it applies at the boundary of the domain without a case split.

The second estimate is the loss of the function at a value x that gives up an amount t: the tangent line at x - t bounds the loss by -t * (log (x - t) + 1), and the hypothesis t ≤ x / 2, which bounds log (x - t) from below by log x - log 2, is where the constant log 2 of the statement comes from. It is stated for t = 0, and for the x = 0 that the hypotheses then force, so that a caller whose amount t may vanish needs no separate case.

The third estimate quantifies the first. The gap u * log u - a * log a - (u - a) * (log a + 1) equals u * log (u / a) - u + a, the integrand of a relative entropy, and (√u - √a) ^ 2 is the integrand of a squared Hellinger distance, so it is the pointwise comparison of these two divergences. It is what makes relative entropy quantitatively strictly convex.

theorem Real.mul_log_sub_mul_log_ge (a u : ℝ) (ha : 0 < a) (hu : 0 ≤ u) : u * log u - a * log a ≥ (u - a) * (log a + 1)

The supporting line of the convex function u ↦ u * log u at a positive point a lies below the graph at every nonnegative u: with the slope log a + 1 of Real.deriv_mul_log, u * log u - a * log a ≥ (u - a) * (log a + 1).

theorem Real.sub_mul_log_le {x t : ℝ} (ht0 : 0 ≤ t) (htx : t ≤ x / 2) : (x - t) * log (x - t) - x * log x ≤ -t * (log x - log 2 + 1)

The loss of the function u ↦ u * log u at a value x that gives up an amount t, where 0 ≤ t and t ≤ x / 2, is at most -t * (log x - log 2 + 1): the supporting line Real.mul_log_sub_mul_log_ge at x - t bounds the loss by -t * (log (x - t) + 1), and x - t ≥ x / 2 bounds log (x - t) from below by log x - log 2.

The case x = 0, which the hypotheses force together with t = 0 and which makes both sides zero, is included.

theorem TauCeti.sq_sqrt_sub_sqrt_le_mul_log_sub_mul_log_sub {a u : ℝ} (ha : 0 < a) (hu : 0 ≤ u) : (√u - √a) ^ 2 ≤ u * Real.log u - a * Real.log a - (u - a) * (Real.log a + 1)

The gap between the convex function u ↦ u * log u and its supporting line at a positive point a dominates the squared difference of square roots: for every nonnegative u, (√u - √a) ^ 2 ≤ u * log u - a * log a - (u - a) * (log a + 1). This strengthens Real.mul_log_sub_mul_log_ge; the right side is u * log (u / a) - u + a.