Re: [isabelle] Convex functions formalization -- 2

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.)


Attachment: signature.asc
Description: This is a digitally signed message part.

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