generalized AM-GM

Stream: maths

[Violeta Hernández]

We currently only have AM-GM for sequences of reals in Mathlib. By changing the nth root to an nth power, this inequality is statable in any ordered field (commutative semiring?), and I believe it should stay true.

If the field is algebraically closed, one can simply follow Cauchy's proof (n implies 2n, n + 1 implies n). The issue is that the latter step requires taking an nth root within the induction hypothesis, and thus isn't directly applicable in non-algebraic fields.

Of course, one can simply extend the field to a larger algebraic field (e.g. the surreals) and finish the proof there. But this is quite the sledgehammer and would probably be difficult to state in Lean.

[Violeta Hernández]

So basically, what can we use to prove AM-GM for ordered fields in Lean?

[Violeta Hernández]

(unfortunately AM-GM can't be reduced to a sum of squares the same way e.g. Cauchy-Schwarz can, see the Motzkin polynomial)

[Kevin Buzzard]

What's the statement you want to prove?

[Violeta Hernández]

$$\left(\frac{\sum_{i=1}^n x_i}{n}\right)^n \ge \prod_{i=1}^n x_i$$

[Violeta Hernández]

But actually I think I made a mistake in my proof. The Wikipedia induction proofs work just fine over an ordered field, just by taking out the nth root

[Violeta Hernández]

Obviously we still want the weighted version with real numbers, because arbitrary powers don't make sense in an arbitrary field. But I think this version would be cool to have as well.

[Violeta Hernández]

(just to make sure, we don't have it, do we?)

[Eric Wieser]

Presumably you also want this with an $n^n$ term moved to the RHS, so that it holds in rings?

[Violeta Hernández]

Oh, of course

[Violeta Hernández]

I'll just have to make sure the proof still works