Minimum Product Sets of Positive Reals
Abstract
A finite set of positive real numbers with the least possible number of products is a geometric progression.
Theorem 1.1 (The ordered-product lower bound).
Proof. Machine-checked in Lean as D5/S3/Arith/GeometricProductSetMinimum.product_card_lower_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let A be a nonempty finite set of positive real numbers, of size m. Then AA has at least 2m-1 elements. In increasing coordinates x_0<…<x_(m-1), the products along an increasing grid path from (0,0) to (m-1,m-1) are strictly increasing. Such a path has 2m-1 vertices.
Theorem 1.2 (Equality forces constant consecutive ratios).
Proof. Machine-checked in Lean as D5/S3/Arith/GeometricProductSetMinimum.eq_geometric_of_product_card (✓ std3). ∎
Source. Repository-derived.
Commentary.
Suppose A contains at least two positive real numbers and AA has at most 2|A|-1 elements. The lower bound gives equality. Every increasing product-grid path therefore enumerates AA in increasing order. Compare the path that first follows row zero with the path that changes from row zero to row one at column j-1. Their entries at position j agree, giving x_0 x_j=x_1 x_(j-1). Thus x_j=x_0(x_1/x_0)^j for every index j, and x_1/x_0>1.