Zulip Chat Archive

Stream: new members

Topic: Try to formalize a high school math problem

Jz Pan (Nov 23 2020 at 17:59):

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

Kevin Buzzard (Nov 23 2020 at 18:04):

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

Jz Pan (Nov 23 2020 at 18:05):

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

Jz Pan (Nov 23 2020 at 18:09):

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 (Nov 24 2020 at 02:27):

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 (Nov 24 2020 at 03:12):

The problem description:

Let a,b,tRa,b,t\in\mathbb{R} be positive such that aba\neq b, a=tb3a=tb^3, and aa=bba^a=b^b.
(1) If t=4t=4, prove that 1/e+4/e3<a+b<11/e+4/e^3 < a+b < 1.
(2) Assume moreover that a+b>2/ta+b>2/\sqrt{t}. View a,ba,b as functions of tt and denote g(t)=a+bg(t)=a+b.
Compute the range of tt and prove that g(t)g(t) increases as tt increases.

Jz Pan (Nov 24 2020 at 03:32):

The solution to problem 1:

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

  • bb decreases and tt increases as aa increases,
  • either a(0,1/e),b(1/e,1),t(0,e2)a\in(0,1/e),b\in(1/e,1),t\in(0,e^2), or a(1/e,1),b(0,1/e),t(e2,+)a\in(1/e,1),b\in(0,1/e),t\in(e^2,+\infty).
  • If a>ba > b, then 1/t=b3/a<b3/b=b1/\sqrt{t}=\sqrt{b^3/a} < \sqrt{b^3/b}=b and hence a+b>2b>2/ta+b > 2b > 2/\sqrt{t}.
  • If a<ba < b, then 1/t=b3/a>b3/b=b1/\sqrt{t}=\sqrt{b^3/a} > \sqrt{b^3/b}=b and hence a+b<2b<2/ta+b < 2b < 2/\sqrt{t}.

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

Jz Pan (Nov 24 2020 at 03:42):

The solution to problem 2:

It's clear from the above discussion that the range of tt is (e2,+)(e^2,+\infty).
Conversely, when aa goes up from 1/e1/e to 11 the bb goes down from 1/e1/e to 00, and the tt goes up from e2e^2 to ++\infty, hence given any t>e2t>e^2 there exist a,ba,b which satisfy the desired conditions.

Since tt increases as aa increases, we only need to show that gg increases as aa increases, namely d(a+b)/da>0\mathrm{d}(a+b)/\mathrm{d}a>0.
We have d(a+b)/da=1+db/da=1+(dy/da)/(dy/db)=1+(1+loga)/(1+logb)\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+logb<01+\log b<0, we only need to show logb+loga+2<0\log b+\log a+2<0, namely ab<1/e2ab<1/e^2, namely b<1/ae2b<1/ae^2.
Since b<1/eb<1/e and 1/ae2<1/e1/ae^2<1/e, this is equivalent to f(b)>f(1/ae2)f(b)>f(1/ae^2), namely aloga>1ae2(2loga)a \log a > \frac{1}{ae^2}(-2-\log a), note that f(a)=f(b)f(a)=f(b).
This is equivalent to g(x)>0g(x)>0 for x(1/e,1)x\in(1/e,1), where g(x)=(x+1xe2)logx+2xe2g(x)=\left(x+\frac{1}{xe^2}\right)\log x + \frac{2}{xe^2}.
Since g(1/e)=0g(1/e)=0, we only need to show that g(x)>0g'(x)>0 for x(1/e,1)x\in(1/e,1).
This is true since g(x)=...=(11x2e2)(1+logx)g'(x)= ... = \left(1-\frac{1}{x^2e^2}\right)(1+\log x), which is obviously positive if x(1/e,1)x\in(1/e,1).

Jz Pan (Nov 24 2020 at 03:44):

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 d(b)/da\mathrm{d}(b)/\mathrm{d}a.

Heather Macbeth (Nov 24 2020 at 23:06):

@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 (Nov 25 2020 at 04:10):

Thanks, I'll try later.

Last updated: Dec 20 2023 at 11:08 UTC