Lemma 2.
With the setup in (i), write
G
′
n
=
G
n
(
¯
a
1
,
¯
a
2
, a
3
, . . . , a
n
)
and
A
′
n
=
A
n
(
¯
a
1
,
¯
a
2
, a
3
, . . . , a
n
)
.
Then
G
′
n
≥
G
n
and
A
′
n
=
A
n
.
Proof.
We have
G
′
n
=
n
√
¯
a
1
¯
a
2
a
3
. . . a
n
≥
n
√
a
1
a
2
a
3
. . . a
n
=
G
n
,
and
A
′
n
=
1
n
(
¯
a
1
+
¯
a
2
+
a
3
+
· · ·
+
a
n
) =
1
n
(
A
n
+
a
1
+
a
2
−
A
n
+
a
3
+
· · ·
+
a
n
)
=
1
n
(
a
1
+
a
2
+
a
3
+
· · ·
+
a
n
) =
A
n
.
(ii)
Let
a
1
, . . . , a
n
be non-negative real numbers. Lemma 1 tells us either they are all
equal to
A
n
(in which case we are done), or there are
k > 0
elements not equal to
A
n
.
In the latter case, we may rearrange the terms so that
a
1
< A
n
and
a
2
> A
n
and apply
(i) to get ¯
a
1
=
A
n
and ¯
a
2
=
a
1
+
a
2
−
A
n
satisfying, per Lemma 2,
G
′
n
≥
G
n
and
A
′
n
=
A
n
.
Note that
¯
a
1
=
A
n
, so this new set of numbers
¯
a
1
,
¯
a
2
, a
3
, . . . , a
n
has at most
k
−
1
terms
not equal to
A
n
. We may apply Lemma 1 and (i) repeatedly, each application reducing
the number of non-
A
n
terms by at least
1
. Then after at most
k
≤
n
applications, all
n
numbers in our set will be
A
n
.
2
By Lemma 2,
G
′
n
does not decrease on each application, so
G
n
(
A
n
, . . . , A
n
)
≥ · · · ≥
G
n
(
¯
a
1
,
¯
a
2
, a
3
, . . . , a
n
)
≥
G
n
(
a
1
, . . . , a
n
)
.
Now
G
n
(
A
n
, . . . , A
n
) =
n
p
A
n
n
=
A
n
, so we have
G
n
=
G
n
(
a
1
, . . . , a
n
)
≤
G
n
(
A
n
, . . . , A
n
) =
A
n
.
(iii) Let
k
be the number of
a
i
s that are not equal to
A
n
. We claim that
G
n
≤
A
n
for each
k
=
0, . . . , n
.
When
k
=
0
,
a
i
=
A
n
for all
i
and so
G
n
=
n
p
A
n
n
=
A
n
,
and our claim holds.
Let
k
≤
n
−
1
and suppose the claim is true for each
0
≤
j
≤
k
. That is,
G
n
≤
A
n
holds if there are at most
k a
i
s that are not equal to
A
n
.
2
This is the step we are formalizing in (iii).
3