Re: [isabelle] Convex functions formalization -- 2
Sorry, I meant afp.sf.net.
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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and