Classic mathematics

Cauchy–Schwarz in two dimensions

A famous inequality becomes a nonnegative square after one algebraic identity.

-- Top 100 #78: Cauchy–Schwarz in two dimensions
-- History: 19th century · Cauchy and Schwarz.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: In two dimensions, the gap is the square of the determinant ad−bc.
-- Scope: Proves (ac+bd)² ≤ (a²+b²)(c²+d²) for arbitrary integers a,b,c,d. General inner-product spaces are outside this example.
-- Source: https://lurch.plus/100/

theorem cauchy_schwarz_2 (a b c d : Int) :
    (a*c+b*d)^2 ≤ (a*a+b*b)*(c*c+d*d) := by
  have square_nonnegative := Int.sq_nonneg (a*d-b*c)
  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

19th century · Cauchy and Schwarz

In two dimensions, the gap is the square of the determinant ad−bc.

Proves (ac+bd)² ≤ (a²+b²)(c²+d²) for arbitrary integers a,b,c,d. General inner-product spaces are outside this example.

Historical Top 100 list (reproduced by Lurch)

Expected output

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

File checked successfully.

Exercise

Try proportional vectors (a,b)=(2,4) and (c,d)=(3,6). Why does equality hold?