Re: [isabelle] Convex functions formalization -- 2

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.


Tim McKenzie schrieb:
> On Thursday 02 July 2009 22:40:20 grechukbogdan wrote:
>> 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.
> 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
> <><

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.