Finite lower bounds for the largest element

This file derives direct and square-root forms of the largest-element bound from Leo Moser's exact sum-of-squares inequality.

theorem LeanPool.ErdosMoser.erdosMoserMaxBound {A : Finset ℕ} (hA : A.Nonempty) (h : HasDistinctSubsetSums A) : 4 ^ A.card - 1 ≤ 3 * ↑A.card * ↑(A.max' hA) ^ 2

If a nonempty finite set of natural numbers has distinct subset sums, then 4 ^ |A| - 1 ≤ 3 * |A| * max(A) ^ 2.

theorem LeanPool.ErdosMoser.erdosMoserMaxSqrt {A : Finset ℕ} (hA : A.Nonempty) (h : HasDistinctSubsetSums A) : √((4 ^ A.card - 1) / (3 * ↑A.card)) ≤ ↑(A.max' hA)

Square-root form of the finite largest-element bound: sqrt ((4 ^ |A| - 1) / (3 * |A|)) ≤ max(A).