Formalize Leo Moser's finite distinct-subset-sums inequality

LeanPool.lean

@@ -790,6 +790,11 @@ import LeanPool.Erdos403
 import LeanPool.Erdos403.Basic
 import LeanPool.Erdos403.FactBase
 import LeanPool.Erdos403.Sharp
+import LeanPool.ErdosMoser
+import LeanPool.ErdosMoser.Basic
+import LeanPool.ErdosMoser.Bounds
+import LeanPool.ErdosMoser.DiscreteVariance
+import LeanPool.ErdosMoser.SubsetSums
 import LeanPool.ErdosTuzaValtr
 import LeanPool.ErdosTuzaValtr.All
 import LeanPool.ErdosTuzaValtr.Config.Default

LeanPool/ErdosMoser.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 Egor Lyfar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Egor Lyfar
+-/
+
+import LeanPool.ErdosMoser.Bounds
+
+/-!
+# Leo Moser's finite distinct-subset-sums inequality
+
+Source: doi:10.1016/S0304-0208(08)73500-X, url:https://www.erdosproblems.com/1
+Authors: Egor Lyfar
+Status: verified
+Main declarations: `LeanPool.ErdosMoser.leoMoserVarianceBound`
+Tags: additive-combinatorics, number-theory, distinct-subset-sums, erdos-problems
+MSC: 11B13, 11B75
+-/
+
+/-!
+Guy's 1982 account states the exact finite sum-of-squares inequality as
+Theorem 2 and attributes it to Leo Moser. This project formalizes that
+inequality and derives two finite lower bounds for the largest element of a
+set with distinct subset sums.
+
+The stronger historical asymptotic bound attributed jointly to Erdős and
+Moser is not claimed here, and Erdős Problem 1 remains open.
+-/

LeanPool/ErdosMoser/Basic.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Egor Lyfar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Egor Lyfar
+-/
+
+import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+import Mathlib.Algebra.BigOperators.Group.Finset.Powerset
+import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Algebra.BigOperators.Ring.Finset
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Data.Finset.Card
+import Mathlib.Data.Finset.Max
+import Mathlib.Data.Finset.Powerset
+import Mathlib.Data.Real.Basic
+import Mathlib.Tactic.NormNum
+
+/-!
+# Distinct subset sums
+
+This file defines finite sets of natural numbers with distinct subset sums and
+establishes the elementary upper bound on their sum of squares in terms of
+their largest element.
+-/
+
+namespace LeanPool.ErdosMoser
+
+open Finset
+
+/-- A finite set has distinct subset sums if the subset-sum map on its powerset
+is injective. -/
+def HasDistinctSubsetSums (A : Finset ℕ) : Prop :=
+  ∀ S ∈ A.powerset, ∀ T ∈ A.powerset, S.sum id = T.sum id → S = T
+
+/-- The powerset of a finite set has cardinality `2 ^ A.card`. -/
+theorem powersetCardEqTwoPow (A : Finset ℕ) :
+    A.powerset.card = 2 ^ A.card := by
+  rw [Finset.card_powerset]
+
+/-- The sum of the squared elements of a nonempty finite set is at most its
+cardinality times the square of its largest element. -/
+lemma sumSquaresLeCardMulMaxSquare {A : Finset ℕ} (hA : A.Nonempty) :
+    ∑ a ∈ A, (a : ℝ) ^ 2 ≤ A.card * ((A.max' hA : ℕ) : ℝ) ^ 2 := by
+  have hPointwise : ∀ a ∈ A, (a : ℝ) ^ 2 ≤ ((A.max' hA : ℕ) : ℝ) ^ 2 := by
+    intro a ha
+    have hLe : a ≤ A.max' hA := A.le_max' a ha
+    have hLeReal : (a : ℝ) ≤ ((A.max' hA : ℕ) : ℝ) := by
+      exact_mod_cast hLe
+    have hNonnegative : (0 : ℝ) ≤ (a : ℝ) := by
+      exact_mod_cast Nat.zero_le a
+    exact pow_le_pow_left₀ hNonnegative hLeReal 2
+  have hSum := Finset.sum_le_card_nsmul A (fun a ↦ (a : ℝ) ^ 2)
+    (((A.max' hA : ℕ) : ℝ) ^ 2) hPointwise
+  simpa [nsmul_eq_mul, mul_comm] using hSum
+
+end LeanPool.ErdosMoser

LeanPool/ErdosMoser/Bounds.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2026 Egor Lyfar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Egor Lyfar
+-/
+
+import LeanPool.ErdosMoser.SubsetSums
+import Mathlib.Analysis.Real.Sqrt
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+
+/-!
+# 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.
+-/
+
+namespace LeanPool.ErdosMoser
+
+open Finset
+
+/-- If a nonempty finite set of natural numbers has distinct subset sums, then
+`4 ^ |A| - 1 ≤ 3 * |A| * max(A) ^ 2`. -/
+theorem erdosMoserMaxBound {A : Finset ℕ} (hA : A.Nonempty)
+    (h : HasDistinctSubsetSums A) :
+    (4 : ℝ) ^ A.card - 1 ≤
+      3 * A.card * ((A.max' hA : ℕ) : ℝ) ^ 2 := by
+  have hVariance :
+      (4 : ℝ) ^ A.card - 1 ≤ 3 * ∑ a ∈ A, (a : ℝ) ^ 2 :=
+    leoMoserVarianceBound h
+  have hUpper :
+      ∑ a ∈ A, (a : ℝ) ^ 2 ≤
+        A.card * ((A.max' hA : ℕ) : ℝ) ^ 2 :=
+    sumSquaresLeCardMulMaxSquare hA
+  have hScaled :
+      3 * ∑ a ∈ A, (a : ℝ) ^ 2 ≤
+        3 * (A.card * ((A.max' hA : ℕ) : ℝ) ^ 2) := by
+    linarith
+  linarith
+
+/-- Square-root form of the finite largest-element bound:
+`sqrt ((4 ^ |A| - 1) / (3 * |A|)) ≤ max(A)`. -/
+theorem erdosMoserMaxSqrt {A : Finset ℕ} (hA : A.Nonempty)
+    (h : HasDistinctSubsetSums A) :
+    Real.sqrt (((4 : ℝ) ^ A.card - 1) / (3 * A.card)) ≤
+      ((A.max' hA : ℕ) : ℝ) := by
+  have hCardPositive : (0 : ℝ) < A.card := by
+    have : 0 < A.card := Finset.card_pos.mpr hA
+    exact_mod_cast this
+  have hDenominatorPositive : (0 : ℝ) < 3 * A.card := by
+    linarith
+  have hMain :
+      (4 : ℝ) ^ A.card - 1 ≤
+        3 * A.card * ((A.max' hA : ℕ) : ℝ) ^ 2 :=
+    erdosMoserMaxBound hA h
+  have hMaxNonnegative : (0 : ℝ) ≤ ((A.max' hA : ℕ) : ℝ) := by
+    exact_mod_cast Nat.zero_le _
+  have hSquare :
+      ((4 : ℝ) ^ A.card - 1) / (3 * A.card) ≤
+        ((A.max' hA : ℕ) : ℝ) ^ 2 := by
+    rw [div_le_iff₀ hDenominatorPositive]
+    linarith
+  exact (Real.sqrt_le_left hMaxNonnegative).mpr hSquare
+
+end LeanPool.ErdosMoser