A tricky lower bound proof
[examples Isar formalised mathematics analysis The previous post concerned exact numerical calculations, culminating in an example of establishing – automatically – a numerical lower bound for a simple mathematical formula. Although automation is the key to the success of formal verification, a numerical approach is not always good enough. In that example, we could get three significant digits quickly, four significant digits slowly and the exact lower bound never. As every calculus student knows, to locate a minimum or maximum you take the derivative and solve for the point at which it vanishes. The desired property can then be shown using the main value theorem. Let’s do it!
A simple problem with surprising complications
Our task is simply to find the minimum of the function $x\ln x$ for $x\ge0$. And the first question is whether $x\ln x$ is even defined when $x=0$. A purist would say that it is not, because $\ln 0$ is undefined and multiplying $\ln 0$ by $0$ does not help matters. However, most mathematicians would say that $x\ln x$ has a removable singularity at zero. That means that we can define it at the singularity so that it is continuous. The function certainly looks continuous:
The derivative of $x\ln x$ is $\ln x+1$, which goes to zero when $x=1/e$. At that point, $x\ln x$ achieves its minimum, namely $-1/e$. Proving this fact formally, for all $x\ge0$, is tricky because that derivative is certainly undefined when $x=0$. The way around the problem involves proving that $x\ln x$ is continuous for all $x\ge0$.
Proving continuity
We prove the continuity of $x\ln x$ in separate stages: first, simply for $x=0$.
lemma continuous_at_0: "continuous (at_right 0) (λx::real. x * ln x)" unfolding continuous_within by real_asymp
Unfolding continuous_within reduces the continuity claim to the limit claim
$x\ln x \longrightarrow 0\ln 0$, which of course is simply
$x\ln x\longrightarrow0$. Such limits are trivially proved by
Manuel Eberl’s wonderful real_asymp proof method,
which will surely be the subject
of a future blogpost.
From this result, we can quickly prove continuity for all $x\ge0$.
Incorporating the zero case requires a little black magic (the topological definition of continuity), while the non-zero case is straightforward.
lemma continuous_nonneg: fixes x::real assumes "x ≥ 0" shows "continuous (at x within {0..}) (λx. x * ln x)" proof (cases "x = 0") case True with continuous_at_0 show ?thesis by (force simp add: continuous_within_topological less_eq_real_def) qed (auto intro!: continuous_intros)
This result is then repackaged in a more convenient form for later use,
replacing the “at-within” filter by the obvious closed half-interval.
It would be preferable to incorporate the two lemmas above into the body
of continuous_on_x_ln; I have split them up here simply to ease the presentation.
lemma continuous_on_x_ln: "continuous_on {0..} (λx::real. x * ln x)" unfolding continuous_on_eq_continuous_within using continuous_nonneg by blast
Remark: the identical proof works for the continuity of the function $x\sin(1/x)$, but not of $x\exp(1/x)$, even though all three functions have a singularity at $x=0$. What is the essential difference?
Proving the lower bound claim
The first step is to prove that the derivative of $x\ln x$
is indeed $\ln x+1$.
In Isabelle/HOL, calculating a derivative is easy.
If you know the derivative already (perhaps from a computer algebra system),
then verifying the result is even easier.
The technique, already illustrated in an earlier post,
relies on Isabelle’s inbuilt Prolog-like proof calculus.
Repeated application of rules from the list derivative_eq_intros
constructs the derivative and sometimes can simplify it
or prove that it equals a derivative already supplied.
lemma xln_deriv: fixes x::real assumes "x > 0" shows "((λu. u * ln(u)) has_real_derivative ln x + 1) (at x)" by (rule derivative_eq_intros refl | use assms in force)+
We will use this derivative in the main proof, which for clarity is presented in chunks. First, here’s the theorem statement itself:
theorem x_ln_lowerbound: fixes x::real assumes "x ≥ 0" shows "x * ln(x) ≥ -1 / exp 1" proof -
Next, define xmin (the $x$-value of the minimum) to be $1/e$,
then show that it is positive, a fact needed later.
define xmin::real where "xmin ≡ 1 / exp 1" have "xmin > 0" by (auto simp: xmin_def)
The claimed result requires a case analysis. The nontrivial cases are $0\le x<1/e$ and $1/e<x$. In the first case, the point is that $\ln x+1$ is negative, with $x\ln x$ decreasing in value to its minimum.
have "x * ln(x) > xmin * ln(xmin)" if "x < xmin" proof (intro DERIV_neg_imp_decreasing_open [OF that] exI conjI) fix u :: real assume "x < u" and "u < xmin" then have "ln u + 1 < ln 1" unfolding xmin_def by (smt (verit, del_insts) assms exp_diff exp_less_cancel_iff exp_ln_iff) then show "ln u + 1 < 0" by simp next show "continuous_on {x..xmin} (λu. u * ln u)" using continuous_on_x_ln continuous_on_subset assms by fastforce qed (use assms xln_deriv in auto)
The second case is symmetric. The derivative is positive, with $x\ln x$ increasing in value from its minimum. In both cases, continuity is a requirement.
moreover have "x * ln(x) > xmin * ln(xmin)" if "x > xmin" proof (intro DERIV_pos_imp_increasing_open [OF that] exI conjI) fix u assume "x > u" and "u > xmin" then show "ln u + 1 > 0" by (smt (verit, del_insts) ‹0 < xmin› exp_minus inverse_eq_divide ln_less_cancel_iff ln_unique xmin_def) next show "continuous_on {xmin..x} (λu. u * ln u)" using continuous_on_x_ln continuous_on_subset xmin_def by fastforce qed (use ‹0 < xmin› xln_deriv in auto)
If $x=1/e$, then the minimum value equals $-1/e$. Note how the previous results are collected using the keyword moreover.
moreover have "xmin * ln(xmin) = -1 / exp 1" using assms by (simp add: xmin_def ln_div)
The keyword ultimately takes the previous result and the earlier two saved by moreover, delivering them to the following proof.
As we have covered all the cases for $x$, the conclusion follows immediately.
ultimately show ?thesis using eq by fastforce qed
Finally, a numerical conclusion
In the previous post,
we used the approximation proof method (which operates by interval arithmetic) to calculate the minimum as -0.3679,
and it was slow (19 seconds on my zippy laptop).
Now we can get 17 significant figures more or less instantaneously.
corollary fixes x::real assumes "x ≥ 0" shows "x * ln(x) ≥ -0.36787944117144233" (is "_ ≥ ?rhs") proof - have "(-1::real) / exp 1 ≥ ?rhs" by (approximation 60) with x_ln_lowerbound show ?thesis using assms by force qed
If you fancy a challenge, try the same exercise with the function $x\sin(1/x)$. In many ways it’s similar, but the derivative hits zero infinitely often and the formula, $\sin(1/x) - \cos(1/x)/x$, doesn’t look easy to work with. If any of you tackle this problem, send it to me: the first nice solution will be posted here. [Note added 2025-03-19: it is in its own post.]
The examples for this post are online here.
Many thanks to Manuel Eberl for the continuity proof!