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: )

[Pjotr Buys]

For fun and exercise I decided to come back to this and prove that the function is convex. I now also have a fully formalized proof of Theorem 1 of Shearer. Convexity of that function took the longest time by far for me. I basically followed the "pen and paper" proof I wrote above.

The project is available at https://github.com/Pjotr5/ShearerTriangleFreeInd. Not sure if anyone else is interested, but happy to post it elsewhere if so.

[Yaël Dillies]

Would be great to have it in mathlib! Would avoid repeating the above history

[Pjotr Buys]

I would be happy to do that. Do you have advice on how to go about this? I have never added something to Mathlib before. For instance, I tried to work neatly, but I know that I was sloppy here and there. So there is for sure stuff in there that does not adhere to the mathlib style guide. Should I try to fix that before opening a PR?

Also, where in mathlib would something like this go?

[Jeremy Tan]

Just push your PR and we'll help you (not me probably, but Yaël can)

[Jeremy Tan]

But for reviewability try and keep it to 500 added lines per PR or so

[Bryan Gin-ge Chen]

We have a guide for contributors that you may have already seen: #contrib. Regarding style etc., if there's anything you can fix on your own before opening the PR, that will speed up the process, but don't stress out about it too much since it's your first PR.

[Bhavik Mehta]

I'd be very happy to help and review this, especially since I have a pretty clear idea of how this code should look! Congrats on finishing :)

[Pjotr Buys]

Thanks all :). I will try to get to this tomorrow.

[Pjotr Buys]

I made a PR (#27155). There is undoubtedly still a lot of work to be done before it is up to the standards Mathlib. I am interested in the advice of those with more experience :).