Try to formalize a high school math problem

Stream: new members

[Jz Pan]

Currently I'm stuck at telling Lean to calculate the derivative of implicit functions.

[Kevin Buzzard]

Can you post the code which defines the function you want to differentiate?

[Jz Pan]

Sure. This is the file I'm working, but I haven't define the final implicit function yet. test001.lean

[Jz Pan]

The idea of proof of problem 2 in that file is not quite correct (which tries to avoid differentiating implicit functions), and I have to revert to the human-readable proof now.

[Jz Pan]

Oops. It looks like that the post containing the problem description itself is failed to send. I'm sorry. Will try to repost as soon as possible.

[Jz Pan]

The problem description:

Let $a,b,t\in\mathbb{R}$ be positive such that $a\neq b$, $a=tb^3$, and $a^a=b^b$.
(1) If $t=4$, prove that $1/e+4/e^3 < a+b < 1$.
(2) Assume moreover that $a+b>2/\sqrt{t}$. View $a,b$ as functions of $t$ and denote $g(t)=a+b$.
Compute the range of $t$ and prove that $g(t)$ increases as $t$ increases.

[Jz Pan]

The solution to problem 1:

Let $y=f(x)=x \log x$ for $x>0$, then $f(x)<0$ when $x<1$, $f(x)=0$ when $x=1$, and $f(x)>0$ when $x>1$.
We have $f'(x)=1+\log x$, which satisfies $f'(x)<0$ when $x<1/e$, and $f'(x)>0$ when $x>1/e$.
Therefore $f(x)$ decreases as $x$ increases if $x\in(0,1/e)$, $f(x)$ increases as $x$ increases if $x\in(1/e, +\infty)$, and $f(x)$ takes minimun at $x=1/e$ with value $-1/e$.
Therefore if $a\neq b$ such that $a^a=b^b$, then $f(a)=f(b)=:y$, we must have $y\in(-1/e,0)$, $a,b\in(0,1/e)\cup(1/e,1)$, and

• $b$ decreases and $t$ increases as $a$ increases,
• either $a\in(0,1/e),b\in(1/e,1),t\in(0,e^2)$, or $a\in(1/e,1),b\in(0,1/e),t\in(e^2,+\infty)$.
• If $a > b$, then $1/\sqrt{t}=\sqrt{b^3/a} < \sqrt{b^3/b}=b$ and hence $a+b > 2b > 2/\sqrt{t}$.
• If $a < b$, then $1/\sqrt{t}=\sqrt{b^3/a} > \sqrt{b^3/b}=b$ and hence $a+b < 2b < 2/\sqrt{t}$.

The (1) comes from that since $t=4 < e^2$, we have $a < 1/e < b$,
hence $a+b < 2/\sqrt{t}=1$ and $a+b=tb^3+b>t/e^3+1/e=1/e+4/e^3$.

[Jz Pan]

The solution to problem 2:

It's clear from the above discussion that the range of $t$ is $(e^2,+\infty)$.
Conversely, when $a$ goes up from $1/e$ to $1$ the $b$ goes down from $1/e$ to $0$, and the $t$ goes up from $e^2$ to $+\infty$, hence given any $t>e^2$ there exist $a,b$ which satisfy the desired conditions.

Since $t$ increases as $a$ increases, we only need to show that $g$ increases as $a$ increases, namely $\mathrm{d}(a+b)/\mathrm{d}a>0$.
We have $\mathrm{d}(a+b)/\mathrm{d}a=1+\mathrm{d}b/\mathrm{d}a=1+(\mathrm{d}y/\mathrm{d}a)/(\mathrm{d}y/\mathrm{d}b)=1+(1+\log a)/(1+\log b)$.
Since $1+\log b<0$, we only need to show $\log b+\log a+2<0$, namely $ab<1/e^2$, namely $b<1/ae^2$.
Since $b<1/e$ and $1/ae^2<1/e$, this is equivalent to $f(b)>f(1/ae^2)$, namely $a \log a > \frac{1}{ae^2}(-2-\log a)$, note that $f(a)=f(b)$.
This is equivalent to $g(x)>0$ for $x\in(1/e,1)$, where $g(x)=\left(x+\frac{1}{xe^2}\right)\log x + \frac{2}{xe^2}$.
Since $g(1/e)=0$, we only need to show that $g'(x)>0$ for $x\in(1/e,1)$.
This is true since $g'(x)= ... = \left(1-\frac{1}{x^2e^2}\right)(1+\log x)$, which is obviously positive if $x\in(1/e,1)$.

[Jz Pan]

Currently I finished formalizing the proof of problem 1, and working on problem 2. I'm wondering that how to tell Lean to calculate the implicit derivative $\mathrm{d}(b)/\mathrm{d}a$.

[Heather Macbeth]

@Jz Pan mathlib has the implicit function theorem: docs#has_strict_fderiv_at.implicit_function. It's phrased very abstractly, but in principle, the result you need can be deduced from this.

[Jz Pan]

Thanks, I'll try later.