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.

50 sentences. 10 compiled into 7 claims and 1 definition. Of the claims, 4 are derived from the results they cite, 0 are checked by the companion Lean development, 1 is false as stated, and 2 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

Abstract

We show that a positive real number and its reciprocal never sum to less than two, and that the sum is smallest at the number one. The proof rests on a single identity, which writes the excess of the sum over two as a square divided by the number. The note also demonstrates Leanify: every definition, every statement and every step of every proof below is compiled from this text to Lean and checked by the Lean kernel.

1. Introduction

How short can the perimeter of a rectangle of area one be? If one side of such a rectangle is long, the other is short, and the question is which proportions balance the two. 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]. For two numbers the inequality has a proof of one line, and we give it in a form that leaves nothing implicit. Theorem 3.1 states the bound, and Corollary 3.2 identifies the number at which the sum is least. Both follow from Lemma 2.1, which expresses the excess of the sum over two as a square divided by a positive number.

The note is written as an ordinary article, and it is also read by Leanify. Every definition and every sentence of a lemma, theorem, corollary or proof has one fixed formal reading, which is compiled to Lean, and every step of a proof is checked against the earlier steps and the results it cites. The other sentences, like this one, motivate, explain and give context. They are prose, which Lean does not check, and no result depends on them. The web reader of the note marks every sentence with what Lean checked for it, and the margin of the typeset note marks every result.

Section 2 introduces the function that measures the sum and proves the identity. Section 3 deduces the bound and the minimum, and Section 4 places them among the classical inequalities between means.

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)>2.

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.