Skip to article
LeanifyA number and its reciprocal

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.

36 sentences. 10 compiled into 7 claims and 1 definition. Of the claims, 7 are derived from the results they cite, 0 are 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: · ·

A number and its reciprocal

Leanify demo

Published source · Verification map

Contents
  1. 1. Introduction
  2. 2. An identity
  3. 3. The bound and its minimum
  4. 4. Arithmetic and geometric means

1. Introduction

How short can the perimeter of a rectangle of area one be? Half the perimeter is the length of one side plus its reciprocal, so the question asks how small a positive number and its reciprocal can be together. The answer is the square: the sum is never below two, and it equals two when both sides have length one. This is the simplest case of the inequality between the arithmetic and the geometric mean, which goes back at least to Cauchy [2] and to which a large literature is devoted [1, 3].

2. An identity

We study the sum of a positive number and its reciprocal as a function of the number. Define f:(0,∞)→Rf:(0,\infty)\to\mathbb{R} by f(x)≔x+1xf(x)\coloneqq x+\frac1x. The domain matters: the reciprocal is not defined at zero, and negative numbers behave differently, as Section 4 explains.

To compare the sum with two, we bring their difference to a common denominator, where a perfect square appears in the numerator.

Lemma 2.1.

For every x∈(0,∞)x\in(0,\infty), f(x)−2=(x−1)2xf(x)-2=\frac{(x-1)^2}{x}.

Proof.

Let x∈(0,∞)x\in(0,\infty). Then f(x)−2=x+1x−2=x2−2x+1x=(x−1)2xf(x)-2=x+\frac1x-2=\frac{x^2-2x+1}{x}=\frac{(x-1)^2}{x}.

□

The identity turns the bound into a question about the sign of a quotient.

3. The bound and its minimum

A square is never negative, and dividing it by a positive number keeps it so. Together with Lemma 2.1, this proves the bound.

Theorem 3.1.

For every x∈(0,∞)x\in(0,\infty), f(x)≥2f(x)\ge2.

Proof.

Let x∈(0,∞)x\in(0,\infty). Then (x−1)2x≥0\frac{(x-1)^2}{x}\ge0. By Lemma 2.1, f(x)−2=(x−1)2x≥0f(x)-2=\frac{(x-1)^2}{x}\ge0.

□

The bound cannot be improved, because the number one attains it. Its reciprocal is itself, so the sum there is exactly two, and the theorem shows that no other number does better.

Corollary 3.2.

For every x∈(0,∞)x\in(0,\infty), f(1)≤f(x)f(1)\le f(x).

Proof.

By Theorem 3.1, f(1)=2≤f(x)f(1)=2\le f(x) for every x∈(0,∞)x\in(0,\infty).

□

In the language of the introduction, among all rectangles of area one the square has the least perimeter.

4. Arithmetic and geometric means

For two positive numbers, the arithmetic mean is at least the geometric mean [3]. A number and its reciprocal have geometric mean one, so for them this inequality is Theorem 3.1. Conversely, applying the theorem to the square root of the ratio of two positive numbers gives the inequality between their arithmetic and geometric mean. For more than two numbers the proofs take more work. Cauchy's proof proceeds by a forward and backward induction on the number of terms, and Hurwitz [4] extended the idea of Lemma 2.1 to any number of terms, with a sum of squares in place of a single square. These and many other proofs are collected in [1, 5].

The positivity of the number cannot be dropped. For a negative number both terms are negative, and the sum is at most minus two. The definition of the function therefore states its domain, and Lean checks that the reciprocal is only ever taken of a positive number.

References

  1. P. S. Bullen, Handbook of Means and Their Inequalities, Kluwer Academic Publishers, Dordrecht, 2003.
  2. A.-L. Cauchy, Cours d'analyse de l'École royale polytechnique, Paris, 1821.
  3. G. H. Hardy, J. E. Littlewood and G. Pólya, Inequalities, 2nd edition, Cambridge University Press, 1952.
  4. A. Hurwitz, Ueber den Vergleich des arithmetischen und des geometrischen Mittels, Journal für die reine und angewandte Mathematik 108 (1891), 266–268.
  5. J. M. Steele, The Cauchy–Schwarz Master Class, Cambridge University Press, 2004.