Re: [isabelle] Convex functions formalization -- 2



Thanks for that link.

Tim
<><

On Sunday 05 July 2009 02:15:23 Tobias Nipkow wrote:
> 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
> > <><

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



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