Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: a classic proof by Pólya

Email Gateway (Jul 11 2022 at 13:13):

From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce a new entry by Manuel Eberl:

Pólya’s Proof of the Weighted Arithmetic–Geometric Mean Inequality

This article provides a formalisation of the Weighted Arithmetic–Geometric Mean Inequality for given non-negative reals and non-negative weights. … I follow Pólya's elegant proof .... Pólya claims that this proof came to him in a dream, and that it was “the best mathematics he had ever dreamt.”

Now online at https://www.isa-afp.org/entries/Weighted_Arithmetic_Geometric_Mean.html

Larry

Last updated: Feb 05 2025 at 16:23 UTC