Stream: new members
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 be positive such that , , and .
(1) If , prove that .
(2) Assume moreover that . View as functions of and denote .
Compute the range of and prove that increases as increases.
Jz Pan (Nov 24 2020 at 03:32):
The solution to problem 1:
Let for , then when , when , and when .
We have , which satisfies when , and when .
Therefore decreases as increases if , increases as increases if , and takes minimun at with value .
Therefore if such that , then , we must have , , and
- decreases and increases as increases,
- either , or .
- If , then and hence .
- If , then and hence .
The (1) comes from that since , we have ,
hence and .
Jz Pan (Nov 24 2020 at 03:42):
The solution to problem 2:
It's clear from the above discussion that the range of is .
Conversely, when goes up from to the goes down from to , and the goes up from to , hence given any there exist which satisfy the desired conditions.
Since increases as increases, we only need to show that increases as increases, namely .
We have .
Since , we only need to show , namely , namely .
Since and , this is equivalent to , namely , note that .
This is equivalent to for , where .
Since , we only need to show that for .
This is true since , which is obviously positive if .
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 .
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: May 07 2021 at 00:30 UTC