Email Gateway (Aug 18 2022 at 13:41): Email Gateway (Aug 18 2022 at 13:41):From: Tobias Nipkow <nipkow@in.tum.de>
By "library" he meant the Archive of Formal Proofs www.afp.sf.
We actively encourage the submission of small self-contained results to
the AFP.
Tobias
Tim McKenzie schrieb:
Email Gateway (Aug 18 2022 at 13:42):From: Tobias Nipkow <nipkow@in.tum.de>
Sorry, I meant afp.sf.net.
Tobias
Tim McKenzie schrieb:
Email Gateway (Aug 18 2022 at 13:45):From: Tim McKenzie <tjm1983@gmail.com>
Thanks for that link.
Tim
<><
On Sunday 05 July 2009 02:15:23 Tobias Nipkow wrote:
signature.asc
Email Gateway (Aug 18 2022 at 13:46):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear members of Isabelle users,
Previous week I have sent you my formalization of some theorems about convex functions. I have received a huge amount of very useful feedback, for which I really thankful.
The main information I received is that some convex analysis (mostly about convex sets, not convex functions) are formalizing in Isabelle now, and my definitions are not exactly match yours. As a result, although many my theorems are new, it is not obvious how to add them to the library.
During last three days, I completely rewrote my theory. I have installed new version of Isabelle, import Convexity_Euclidean_Space.thy, and rewrote my theory based on the definitions and lemmas from that site. All my lemmas which were duplicated are removed from the theory. It was not easy, because I needed properties of convex functions real -> real, and you results were proved for functions real^n -> real, so I needed to play a lot with transformation real^1 to real and back through "vec1".
As a result, I have done this, but I had no time even to start of polishing my proofs. I have received huge amount of valuable suggestions how to make the proofs more readable, but I had no time to apply them. And my academic visit to Edinburgh is finishing today. I am sorry for this.
The new file is attached. The detailed description is presented below.
Sincerely,
Bogdan Grechuk.
*** Updated Description of Convexity.thy ***
First, I proved some simple properties of convex interval on real line, based on general properties of convex sets, proved in Convexity_Euclidean_Space.thy.
Then I introduced a notion of nondecreasing function (the only definition in the theory now), and prove that differentiable function is non-decreasing if and only if its derivative is non-negative.
After this preparation, I started to play with convex functions from real to real. First, I proved that f(g(x)) is convex if f() convex and g() linear, or if f() convex increasing and g() convex, and that the global maximum of convex function on [a, b] is f(a) or f(b). Then I proved some properties of convex functions connected with derivatives. Namely, I proved that graph of convex function is above all the tangents, and used this fact to prove that if the first derivative of convex function at some point is 0, that this point is a global minimum. Then I proved that (twice) differentiable function is convex on an interval if and only if its first derivative is non-decreasing on this interval, and also if and only if its second derivative is non-negative.
Clearly, these theorems provide a powerful tool of proving convexity of different functions. As an example, I used them to prove that -ln(x) is a convex function on (0, infty).
Finally, I use this to prove the generalized (weighted) version of famous Geometric-Arithmetic Mean Inequality, namely that alpha_1 * x_1 + ... + alpha_k x_k >= x_1^alpha_1 * ... * x_k^alpha_k whenever alpha_i>=0 and sum of alpha_i = 1. I hope may be this version is new. It reduces to usual Geometric-Arithmetic Mean Inequality when alpha_1 = ... = alpha_k = 1/k, but this particular case was already proved in the library.
Email Gateway (Aug 18 2022 at 13:51):From: Tim McKenzie <tjm1983@gmail.com>
On Thursday 02 July 2009 22:40:20 grechukbogdan wrote:
I was looking for this in the library recently, but I couldn't
find it. Where is it? (In the end, all I needed was the case
k=2, so it didn't take me long to prove what I needed.)
Tim
<><
signature.asc
Last updated: May 03 2024 at 04:19 UTC