Re: [isabelle] Convex functions formalization -- 2



Sorry, I meant afp.sf.net.

Tobias

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.