Convexity of a specific function

Stream: Is there code for X?

[Pjotr Buys]

Hi all,

I am trying to formalize Shearer's lower bound on the independent set number of triangle-free graphs (https://doi.org/10.1016/0012-365X(83)90273-X). My question is about the only 'nontrivial' real analysis step involved, namely the following. I have defined the following function:

import Mathlib

noncomputable def f : ℝ → ℝ
    := fun x ↦ if x = 1 then 1/2 else (x * Real.log x - x + 1) / (x - 1)^2

Moreover, I have explicitly calculated its derivative.

noncomputable def df : ℝ → ℝ
    := fun x ↦ if x = 1 then -1/6 else (-2 + 2*x - Real.log x - x * Real.log x) / (x - 1)^3

My goal is to prove the following statement:

lemma f_convex : ∀ x y, 0 ≤ x → 0 < y → f x ≥ f y + (df y) * (x - y) := by
  sorry

A pen and paper proof would be something like this: The function f is analytic on $\mathbb{R}_{>0}$ because the singularity at $x = 1$ is removable. By explicit calculation it is not hard to see (but also not trivial) that df is its derivative and $f''(x)$ is nonnegative for all nonnegative $x$. Therefore $f$ is convex and thus the inequality holds for all $0 < x$, $0 < y$. By continuity it also holds for $x = 0$.

Does anybody have any advice how to approach this problem in Lean? My instinct is just to intro x and y and start playing around with cases (e.g. x = 0, x < 1, x = 1, 1 < x, y < 1, y = 1, 1 < y, x < y, y <= x) and explicitly proving it (hopefully using some mild bounds on the logarithm). But ideally I would do something that resembles the pen and paper proof more. In fact, for my purposes I don't need to explicitly define df, I just want it to represent the derivative of f.

Any comment is appreciated. Maybe there is some example I can look at of an analysis done involving explicit real functions and their derivatives.

[Yaël Dillies]

Hey! Just FYI @Bhavik Mehta did most of it

[Pjotr Buys]

Ah, that's very nice. I am also quite far into the proof, except for this analysis and some counting stuff. It would be very educational for me to see someone else's (especially someone with so much more experience).

I tried to look around a bit before starting, searching Shearer and off-diagonal Ramsey numbers R(3,t) etc, but I didn't find it. Is it publicly available?

[Yaël Dillies]

It might just be an uncommitted file on Bhavik's laptop :sweat:

[Bhavik Mehta]

I had stored it very safely in a pushed branch of some repository somewhere, but I can't for the life of me find it, so it should technically be public but I have no idea where. For me, I just calculated the second derivative, with a bunch of squeeze theorem calculations to handle the removable discontinuity at 1. I did indeed fully formalise Theorem 1 from the paper you linked.
(I keep looking for this file every month or so, and I always get sad that it's lost :sad: )