Classic mathematics

Arithmetic & geometric means

A nonnegative square is enough to explain why the arithmetic mean dominates the geometric mean.

-- Top 100 #38: Arithmetic & geometric means
-- History: Date unspecified in the list · Cauchy / Pólya proofs.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: The difference between the two sides is a perfect square.
-- Scope: Proves 4ab ≤ (a+b)² over all integers. For nonnegative a,b this is the squared two-variable AM–GM inequality.
-- Source: https://lurch.plus/100/

theorem two_variable_am_gm (a b : Int) :
    4*a*b ≤ (a+b)^2 := by
  have square_nonnegative := Int.sq_nonneg (a-b)
  grind

-- Equality occurs when the two inputs agree.
example (a : Int) : 4*a*a = (a+a)^2 := by grind

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`grind`

Combines logical reasoning and polynomial normalization to construct a proof term that Lean checks.

`Int`

Exact integers, including negatives. Unlike Nat subtraction, integer subtraction does not truncate at zero.

Background and proof scope

Date unspecified in the list · Cauchy / Pólya proofs

The difference between the two sides is a perfect square.

Proves 4ab ≤ (a+b)² over all integers. For nonnegative a,b this is the squared two-variable AM–GM inequality.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

File checked successfully.

Exercise

Prove that a² + b² is at least 2ab using the same square.