Skip to article
LeanifyThe harmonic, geometric and arithmetic mean of two numbers

Single source · compiled by the Lean kernel

This page renders article.tex, the text that the Lean kernel compiled. Each marker reports what the certificate checked for its sentence.

21 sentences. 13 compiled into 16 claims and 5 definitions. Of the claims, 15 are derived from the results they cite, 1 is checked by the companion Lean development, and 0 are unverified. 0 sentences failed to compile, and 0 sentences in results and proofs are prose the grammar does not read yet.

Results whose proof is compiled sentence by sentence: ·

The harmonic, geometric and arithmetic mean of two numbers

Leanify example

Published source · Verification map

Contents
  1. 1. Introduction
  2. 2. The three means

Abstract

For two positive numbers, the harmonic mean is at most the geometric mean, and the geometric mean is at most the arithmetic mean. The geometric and the arithmetic mean agree exactly when the two numbers do. We give the short classical proof, in which every step is derived from what it cites.

1. Introduction

The inequality between the arithmetic and the geometric mean is one of the most frequently used inequalities in analysis, and the monographs [1, 2] discuss it at length. For two numbers it reduces to the fact that a square is nonnegative. The inequality for the harmonic mean then follows from a short computation. Theorem 2 states both, together with the case of equality.

2. The three means

Lemma 1.

Let a,b∈(0,∞)a,b\in(0,\infty). Then a+b2−ab=d22\frac{a+b}{2}-\sqrt{ab}=\frac{d^2}{2}, where d≔a−bd\coloneqq\sqrt a-\sqrt b.

Proof.

We have (a)2=a(\sqrt a)^2=a, (b)2=b(\sqrt b)^2=b and ab=ab\sqrt a\sqrt b=\sqrt{ab}. Hence d22=a−2ab+b2=a+b2−ab\frac{d^2}{2}=\frac{a-2\sqrt{ab}+b}{2}=\frac{a+b}{2}-\sqrt{ab}.

□

Theorem 2.

Let a,b∈(0,∞)a,b\in(0,\infty), and let A≔a+b2A\coloneqq\frac{a+b}{2}, G≔abG\coloneqq\sqrt{ab} and H≔2aba+bH\coloneqq\frac{2ab}{a+b}. Then H≤G≤AH\le G\le A. Moreover, G=AG=A if and only if a=ba=b.

Proof.

By Lemma 1, A−G=(a−b)22≥0A-G=\frac{(\sqrt a-\sqrt b)^2}{2}\ge0. Hence G≤AG\le A, and G=AG=A if and only if a=b\sqrt a=\sqrt b. Moreover, a=b\sqrt a=\sqrt b if and only if a=ba=b, since the square root is injective. Finally, H=G2AH=\frac{G^2}{A}. Since G≤AG\le A and G>0G>0, it follows that H=G⋅GA≤GH=G\cdot\frac{G}{A}\le G.

□

Remark 3.

For a,b∈(0,∞)a,b\in(0,\infty), the quadratic mean Q≔a2+b22Q\coloneqq\sqrt{\frac{a^2+b^2}{2}} is at least the arithmetic mean a+b2\frac{a+b}{2}.

References

  1. G. H. Hardy, J. E. Littlewood and G. Pólya, Inequalities, 2nd ed., Cambridge University Press, 1952.
  2. J. M. Steele, The Cauchy–Schwarz Master Class, Cambridge University Press, 2004.