From 89517512b7308d39b2ba464b73a193874c1e6f5b Mon Sep 17 00:00:00 2001 From: Egor Lyfar Date: Mon, 27 Jul 2026 22:48:06 +0800 Subject: [PATCH 1/3] Formalize Leo Moser's distinct-subset-sums inequality --- LeanPool.lean | 5 + LeanPool/ErdosMoser.lean | 28 +++ LeanPool/ErdosMoser/Basic.lean | 56 +++++ LeanPool/ErdosMoser/Bounds.lean | 66 +++++ LeanPool/ErdosMoser/DiscreteVariance.lean | 294 ++++++++++++++++++++++ LeanPool/ErdosMoser/SubsetSums.lean | 205 +++++++++++++++ LeanPool/projects.yml | 54 ++++ 7 files changed, 708 insertions(+) create mode 100644 LeanPool/ErdosMoser.lean create mode 100644 LeanPool/ErdosMoser/Basic.lean create mode 100644 LeanPool/ErdosMoser/Bounds.lean create mode 100644 LeanPool/ErdosMoser/DiscreteVariance.lean create mode 100644 LeanPool/ErdosMoser/SubsetSums.lean diff --git a/LeanPool.lean b/LeanPool.lean index b067ca79fd..5555837aeb 100644 --- a/LeanPool.lean +++ b/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 diff --git a/LeanPool/ErdosMoser.lean b/LeanPool/ErdosMoser.lean new file mode 100644 index 0000000000..5a9598feaa --- /dev/null +++ b/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. +-/ diff --git a/LeanPool/ErdosMoser/Basic.lean b/LeanPool/ErdosMoser/Basic.lean new file mode 100644 index 0000000000..ab43080671 --- /dev/null +++ b/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 diff --git a/LeanPool/ErdosMoser/Bounds.lean b/LeanPool/ErdosMoser/Bounds.lean new file mode 100644 index 0000000000..6df16c9d4d --- /dev/null +++ b/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 diff --git a/LeanPool/ErdosMoser/DiscreteVariance.lean b/LeanPool/ErdosMoser/DiscreteVariance.lean new file mode 100644 index 0000000000..01119c99e5 --- /dev/null +++ b/LeanPool/ErdosMoser/DiscreteVariance.lean @@ -0,0 +1,294 @@ +/- +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.Basic +import Mathlib.Data.Finset.Sort +import Lean.Elab.Tactic.Omega +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Push +import Mathlib.Tactic.Ring + +/-! +# A sharp variance bound for distinct natural numbers + +The main result of this file minimizes the unnormalized empirical variance of +a finite set of natural numbers. The proof enumerates the set increasingly, +compares all pairwise differences with those of an initial interval, and +evaluates the resulting quadratic sum. +-/ + +namespace LeanPool.ErdosMoser + +open Finset + +/-- Closed form for the sum of squares over `Finset.range m`, stated over the +reals for use in the variance calculation. -/ +lemma sumSquaresRange (m : ℕ) : + 6 * ∑ i ∈ Finset.range m, (i : ℝ) ^ 2 = + (m : ℝ) * ((m : ℝ) - 1) * (2 * (m : ℝ) - 1) := by + induction m with + | zero => simp + | succ n ih => + rw [Finset.sum_range_succ] + push_cast + ring_nf + ring_nf at ih + linarith [ih] + +/-- Pairwise-difference form of the unnormalized variance of a function on a +finite set. -/ +lemma twoMulCardSumSquaresSubSquareEqSumPairsDiffSquare + {ι : Type*} (s : Finset ι) (g : ι → ℝ) : + 2 * ((s.card : ℝ) * (∑ i ∈ s, g i ^ 2) - (∑ i ∈ s, g i) ^ 2) = + ∑ i ∈ s, ∑ j ∈ s, (g i - g j) ^ 2 := by + have hInner : ∀ i ∈ s, + ∑ j ∈ s, (g i - g j) ^ 2 = + (s.card : ℝ) * g i ^ 2 - 2 * g i * (∑ j ∈ s, g j) + + ∑ j ∈ s, g j ^ 2 := by + intro i _ + have hExpand : ∀ j ∈ s, + (g i - g j) ^ 2 = g i ^ 2 + g j ^ 2 - 2 * g i * g j := by + intros + ring + rw [Finset.sum_congr rfl hExpand] + rw [Finset.sum_sub_distrib, Finset.sum_add_distrib, Finset.sum_const, + nsmul_eq_mul] + have hCross : ∑ j ∈ s, 2 * g i * g j = 2 * g i * ∑ j ∈ s, g j := by + rw [← Finset.mul_sum] + rw [hCross] + ring + rw [Finset.sum_congr rfl hInner] + have hRearrange : ∀ i ∈ s, + (s.card : ℝ) * g i ^ 2 - 2 * g i * (∑ j ∈ s, g j) + + ∑ j ∈ s, g j ^ 2 = + ((s.card : ℝ) * g i ^ 2 + ∑ j ∈ s, g j ^ 2) - + 2 * g i * (∑ j ∈ s, g j) := by + intros + ring + rw [Finset.sum_congr rfl hRearrange] + rw [Finset.sum_sub_distrib, Finset.sum_add_distrib, ← Finset.mul_sum] + rw [Finset.sum_const, nsmul_eq_mul] + have hCrossOuter : ∑ i ∈ s, 2 * g i * (∑ j ∈ s, g j) = + (2 * ∑ i ∈ s, g i) * ∑ j ∈ s, g j := by + have hRewrite : ∀ i ∈ s, + 2 * g i * (∑ j ∈ s, g j) = (2 * ∑ j ∈ s, g j) * g i := by + intros + ring + rw [Finset.sum_congr rfl hRewrite, ← Finset.mul_sum] + rw [hCrossOuter] + ring + +/-- A strictly increasing natural-valued sequence grows by at least the +difference of its indices. -/ +lemma strictMonoFinNatLeDiff {m : ℕ} {g : Fin m → ℕ} (hg : StrictMono g) + {i j : Fin m} (h : i ≤ j) : (j : ℕ) - (i : ℕ) ≤ g j - g i := by + suffices hGeneral : ∀ (d : ℕ) (i j : Fin m), (i : ℕ) + d = (j : ℕ) → + d ≤ g j - g i by + have hIndex : (i : ℕ) + ((j : ℕ) - (i : ℕ)) = (j : ℕ) := by + have hValues : (i : ℕ) ≤ (j : ℕ) := h + omega + exact hGeneral ((j : ℕ) - (i : ℕ)) i j hIndex + intro d + induction d with + | zero => + intro i j hEqual + have hValues : (i : ℕ) = (j : ℕ) := by omega + have hIndices : i = j := Fin.ext hValues + subst hIndices + omega + | succ k ih => + intro i j hEqual + have hIntermediateLt : (i : ℕ) + k < m := by + omega + let intermediate : Fin m := ⟨(i : ℕ) + k, hIntermediateLt⟩ + have hIntermediateValue : (intermediate : ℕ) = (i : ℕ) + k := rfl + have hPrevious : k ≤ g intermediate - g i := + ih i intermediate hIntermediateValue.symm + have hIntermediateLtJ : intermediate < j := by + have : (intermediate : ℕ) < (j : ℕ) := by + rw [hIntermediateValue] + omega + exact this + have hStrict : g intermediate < g j := hg hIntermediateLtJ + have hLower : g i ≤ g intermediate := by + have hIndices : i ≤ intermediate := by + have : (i : ℕ) ≤ (intermediate : ℕ) := by + rw [hIntermediateValue] + omega + exact this + exact hg.monotone hIndices + omega + +/-- Increasing a collection of distinct natural numbers can only increase +each squared pairwise difference from that of consecutive indices. -/ +lemma strictMonoFinNatDiffSquareGe {m : ℕ} {g : Fin m → ℕ} (hg : StrictMono g) + (i j : Fin m) : + (((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ^ 2 ≤ + (((g i : ℕ) : ℝ) - ((g j : ℕ) : ℝ)) ^ 2 := by + rcases le_total i j with hij | hji + · have hDifference : (j : ℕ) - (i : ℕ) ≤ g j - g i := + strictMonoFinNatLeDiff hg hij + have hImages : g i ≤ g j := hg.monotone hij + have hIndices : (i : ℕ) ≤ (j : ℕ) := hij + have hDifferenceReal : + ((j : ℕ) : ℝ) - ((i : ℕ) : ℝ) ≤ + ((g j : ℕ) : ℝ) - ((g i : ℕ) : ℝ) := by + have hCast : (((j : ℕ) - (i : ℕ) : ℕ) : ℝ) ≤ + ((g j - g i : ℕ) : ℝ) := by + exact_mod_cast hDifference + rw [Nat.cast_sub hIndices, Nat.cast_sub hImages] at hCast + exact hCast + have hNonnegative : + (0 : ℝ) ≤ ((j : ℕ) : ℝ) - ((i : ℕ) : ℝ) := by + have : ((i : ℕ) : ℝ) ≤ ((j : ℕ) : ℝ) := by + exact_mod_cast hIndices + linarith + have hLeft : + (((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ^ 2 = + (((j : ℕ) : ℝ) - ((i : ℕ) : ℝ)) ^ 2 := by + ring + have hRight : + (((g i : ℕ) : ℝ) - ((g j : ℕ) : ℝ)) ^ 2 = + (((g j : ℕ) : ℝ) - ((g i : ℕ) : ℝ)) ^ 2 := by + ring + rw [hLeft, hRight] + exact pow_le_pow_left₀ hNonnegative hDifferenceReal 2 + · have hDifference : (i : ℕ) - (j : ℕ) ≤ g i - g j := + strictMonoFinNatLeDiff hg hji + have hImages : g j ≤ g i := hg.monotone hji + have hIndices : (j : ℕ) ≤ (i : ℕ) := hji + have hDifferenceReal : + ((i : ℕ) : ℝ) - ((j : ℕ) : ℝ) ≤ + ((g i : ℕ) : ℝ) - ((g j : ℕ) : ℝ) := by + have hCast : (((i : ℕ) - (j : ℕ) : ℕ) : ℝ) ≤ + ((g i - g j : ℕ) : ℝ) := by + exact_mod_cast hDifference + rw [Nat.cast_sub hIndices, Nat.cast_sub hImages] at hCast + exact hCast + have hNonnegative : + (0 : ℝ) ≤ ((i : ℕ) : ℝ) - ((j : ℕ) : ℝ) := by + have : ((j : ℕ) : ℝ) ≤ ((i : ℕ) : ℝ) := by + exact_mod_cast hIndices + linarith + exact pow_le_pow_left₀ hNonnegative hDifferenceReal 2 + +/-- Among finite sets of natural numbers of a fixed cardinality, an initial +interval minimizes the unnormalized empirical variance. -/ +theorem varianceLowerBoundFinsetNat (T : Finset ℕ) : + (T.card : ℝ) ^ 2 * ((T.card : ℝ) ^ 2 - 1) / 12 ≤ + (T.card : ℝ) * (∑ t ∈ T, (t : ℝ) ^ 2) - + (∑ t ∈ T, (t : ℝ)) ^ 2 := by + set m := T.card with hCard + let g : Fin m ↪o ℕ := T.orderEmbOfFin rfl + have hStrict : StrictMono g := g.strictMono + have hSum : + ∑ t ∈ T, (t : ℝ) = ∑ i : Fin m, ((g i : ℕ) : ℝ) := by + rw [← Finset.map_orderEmbOfFin_univ (s := T) rfl, Finset.sum_map] + rfl + have hSumSquares : + ∑ t ∈ T, (t : ℝ) ^ 2 = ∑ i : Fin m, ((g i : ℕ) : ℝ) ^ 2 := by + rw [← Finset.map_orderEmbOfFin_univ (s := T) rfl, Finset.sum_map] + rfl + rw [hSum, hSumSquares] + have hCardUniv : (Finset.univ : Finset (Fin m)).card = m := by + simp + have hVarianceIdentity : + 2 * ((m : ℝ) * (∑ i : Fin m, ((g i : ℕ) : ℝ) ^ 2) - + (∑ i : Fin m, ((g i : ℕ) : ℝ)) ^ 2) = + ∑ i : Fin m, ∑ j : Fin m, + (((g i : ℕ) : ℝ) - ((g j : ℕ) : ℝ)) ^ 2 := by + have h := twoMulCardSumSquaresSubSquareEqSumPairsDiffSquare + (Finset.univ : Finset (Fin m)) (fun i ↦ ((g i : ℕ) : ℝ)) + rw [hCardUniv] at h + exact h + have hPointwise : ∀ i : Fin m, ∀ j : Fin m, + (((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ^ 2 ≤ + (((g i : ℕ) : ℝ) - ((g j : ℕ) : ℝ)) ^ 2 := by + intro i j + exact strictMonoFinNatDiffSquareGe hStrict i j + have hSumLower : + ∑ i : Fin m, ∑ j : Fin m, + (((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ^ 2 ≤ + ∑ i : Fin m, ∑ j : Fin m, + (((g i : ℕ) : ℝ) - ((g j : ℕ) : ℝ)) ^ 2 := + Finset.sum_le_sum (fun i _ ↦ + Finset.sum_le_sum (fun j _ ↦ hPointwise i j)) + have hRangeSum : + ∑ i : Fin m, ∑ j : Fin m, + (((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ^ 2 = + (m : ℝ) ^ 2 * ((m : ℝ) ^ 2 - 1) / 6 := by + have hIdentity : + 2 * ((m : ℝ) * (∑ i : Fin m, ((i : ℕ) : ℝ) ^ 2) - + (∑ i : Fin m, ((i : ℕ) : ℝ)) ^ 2) = + ∑ i : Fin m, ∑ j : Fin m, + (((i : ℕ) : ℝ) - ((j : ℕ) : ℝ)) ^ 2 := by + have h := twoMulCardSumSquaresSubSquareEqSumPairsDiffSquare + (Finset.univ : Finset (Fin m)) (fun i ↦ ((i : ℕ) : ℝ)) + rw [hCardUniv] at h + exact h + have hIndexSum : + (∑ i : Fin m, ((i : ℕ) : ℝ)) = + ∑ i ∈ Finset.range m, (i : ℝ) := by + rw [Fin.sum_univ_eq_sum_range (fun i : ℕ ↦ (i : ℝ))] + have hIndexSquareSum : + (∑ i : Fin m, ((i : ℕ) : ℝ) ^ 2) = + ∑ i ∈ Finset.range m, (i : ℝ) ^ 2 := by + rw [Fin.sum_univ_eq_sum_range (fun i : ℕ ↦ (i : ℝ) ^ 2)] + rw [hIndexSum, hIndexSquareSum] at hIdentity + have hNatIndexSum : + (∑ i ∈ Finset.range m, i) * 2 = m * (m - 1) := + Finset.sum_range_id_mul_two m + have hRealIndexSum : + (∑ i ∈ Finset.range m, (i : ℝ)) * 2 = + (m : ℝ) * ((m : ℝ) - 1) := by + have hCast : (((∑ i ∈ Finset.range m, i) * 2 : ℕ) : ℝ) = + ((m * (m - 1) : ℕ) : ℝ) := by + exact_mod_cast hNatIndexSum + push_cast at hCast + rcases Nat.eq_zero_or_pos m with hm | hm + · simp [hm] + · have hOneLe : 1 ≤ m := hm + simpa [Nat.cast_sub hOneLe] using hCast + have hSquareSum := sumSquaresRange m + rw [hIdentity.symm] + have hTarget : + (m : ℝ) ^ 2 * ((m : ℝ) ^ 2 - 1) / 6 = + 2 * ((m : ℝ) * (∑ i ∈ Finset.range m, (i : ℝ) ^ 2) - + (∑ i ∈ Finset.range m, (i : ℝ)) ^ 2) := by + have hIndexSquare : + (∑ i ∈ Finset.range m, (i : ℝ)) ^ 2 = + ((m : ℝ) * ((m : ℝ) - 1)) ^ 2 / 4 := by + have hSquare : + ((∑ i ∈ Finset.range m, (i : ℝ)) * 2) ^ 2 = + ((m : ℝ) * ((m : ℝ) - 1)) ^ 2 := by + rw [hRealIndexSum] + have hExpand : + ((∑ i ∈ Finset.range m, (i : ℝ)) * 2) ^ 2 = + 4 * (∑ i ∈ Finset.range m, (i : ℝ)) ^ 2 := by + ring + linarith [hExpand ▸ hSquare] + have hIndexSquareFour : + 4 * (∑ i ∈ Finset.range m, (i : ℝ)) ^ 2 = + ((m : ℝ) * ((m : ℝ) - 1)) ^ 2 := by + rw [hIndexSquare] + ring + have hTwelve : + 12 * ((m : ℝ) * (∑ i ∈ Finset.range m, (i : ℝ) ^ 2) - + (∑ i ∈ Finset.range m, (i : ℝ)) ^ 2) = + (m : ℝ) ^ 2 * ((m : ℝ) ^ 2 - 1) := by + calc + 12 * ((m : ℝ) * (∑ i ∈ Finset.range m, (i : ℝ) ^ 2) - + (∑ i ∈ Finset.range m, (i : ℝ)) ^ 2) = + 2 * (m : ℝ) * (6 * ∑ i ∈ Finset.range m, (i : ℝ) ^ 2) - + 3 * (4 * (∑ i ∈ Finset.range m, (i : ℝ)) ^ 2) := by ring + _ = (m : ℝ) ^ 2 * ((m : ℝ) ^ 2 - 1) := by + rw [hSquareSum, hIndexSquareFour] + ring + linarith + linarith + linarith [hVarianceIdentity, hSumLower, hRangeSum] + +end LeanPool.ErdosMoser diff --git a/LeanPool/ErdosMoser/SubsetSums.lean b/LeanPool/ErdosMoser/SubsetSums.lean new file mode 100644 index 0000000000..04f63e6dd6 --- /dev/null +++ b/LeanPool/ErdosMoser/SubsetSums.lean @@ -0,0 +1,205 @@ +/- +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.DiscreteVariance +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Push +import Mathlib.Tactic.Ring + +/-! +# Variance of distinct subset sums + +This file proves the first and second moment identities for subset sums and +combines them with the discrete variance bound to obtain Leo Moser's exact +finite sum-of-squares inequality. +-/ + +namespace LeanPool.ErdosMoser + +open Finset + +/-- Twice the sum of all subset sums is `2 ^ |B|` times the sum of the +elements of `B`. -/ +theorem sumSubsetSums (B : Finset ℕ) (f : ℕ → ℝ) : + 2 * ∑ T ∈ B.powerset, (∑ i ∈ T, f i) = + (2 : ℝ) ^ B.card * ∑ i ∈ B, f i := by + refine Finset.induction_on B ?_ ?_ + · simp + · intro x B hx ih + rw [Finset.sum_powerset_insert hx, Finset.sum_insert hx] + have hInsert : ∀ T ∈ B.powerset, + (∑ i ∈ insert x T, f i) = f x + ∑ i ∈ T, f i := by + intro T hT + have hxT : x ∉ T := fun hxT ↦ hx (Finset.mem_powerset.mp hT hxT) + exact Finset.sum_insert hxT + rw [Finset.sum_congr rfl hInsert] + rw [Finset.sum_add_distrib, Finset.sum_const, Finset.card_powerset, + nsmul_eq_mul] + have hCard : + (2 : ℝ) ^ (insert x B).card = 2 * (2 : ℝ) ^ B.card := by + rw [Finset.card_insert_of_notMem hx, pow_succ] + ring + rw [hCard] + push_cast + linarith [ih] + +/-- Exact second-moment identity for the subset sums of a finite set. -/ +theorem secondMomentSubsetSums (B : Finset ℕ) (f : ℕ → ℝ) : + 4 * ∑ S ∈ B.powerset, (∑ i ∈ S, f i) ^ 2 = + (2 : ℝ) ^ B.card * + ((∑ i ∈ B, f i ^ 2) + (∑ i ∈ B, f i) ^ 2) := by + refine Finset.induction_on B ?_ ?_ + · simp + · intro x B hx ih + rw [Finset.sum_powerset_insert hx] + have hInsertSquare : ∀ T ∈ B.powerset, + (∑ i ∈ insert x T, f i) ^ 2 = + f x ^ 2 + 2 * f x * (∑ i ∈ T, f i) + + (∑ i ∈ T, f i) ^ 2 := by + intro T hT + have hxT : x ∉ T := fun hxT ↦ hx (Finset.mem_powerset.mp hT hxT) + rw [Finset.sum_insert hxT] + ring + rw [Finset.sum_congr rfl hInsertSquare] + rw [Finset.sum_add_distrib, Finset.sum_add_distrib, Finset.sum_const, + Finset.card_powerset, nsmul_eq_mul, ← Finset.mul_sum] + have hFirstMoment := sumSubsetSums B f + have hCard : + (2 : ℝ) ^ (insert x B).card = 2 * (2 : ℝ) ^ B.card := by + rw [Finset.card_insert_of_notMem hx, pow_succ] + ring + have hSumSquares : + (∑ i ∈ insert x B, f i ^ 2) = f x ^ 2 + ∑ i ∈ B, f i ^ 2 := + Finset.sum_insert hx + have hSum : + (∑ i ∈ insert x B, f i) = f x + ∑ i ∈ B, f i := + Finset.sum_insert hx + rw [hCard, hSumSquares, hSum] + push_cast + have hExpand : + (f x + ∑ i ∈ B, f i) ^ 2 = + f x ^ 2 + 2 * f x * (∑ i ∈ B, f i) + + (∑ i ∈ B, f i) ^ 2 := by + ring + rw [hExpand] + have hFirstMomentMul : + 4 * f x * (2 * ∑ T ∈ B.powerset, ∑ i ∈ T, f i) = + 4 * f x * ((2 : ℝ) ^ B.card * ∑ i ∈ B, f i) := by + rw [hFirstMoment] + linarith [ih, hFirstMomentMul] + +/-- Algebraic variance identity for subset sums. -/ +theorem varianceIdentitySubsetSums (B : Finset ℕ) (f : ℕ → ℝ) : + 4 * (∑ S ∈ B.powerset, (∑ i ∈ S, f i) ^ 2) - + (2 : ℝ) ^ B.card * (∑ i ∈ B, f i) ^ 2 = + (2 : ℝ) ^ B.card * ∑ i ∈ B, f i ^ 2 := by + have h := secondMomentSubsetSums B f + linarith [h] + +/-- The image of the subset-sum map has cardinality `2 ^ A.card` when the +subset sums of `A` are distinct. -/ +lemma imageSubsetSumsCard {A : Finset ℕ} (h : HasDistinctSubsetSums A) : + (A.powerset.image (fun S ↦ S.sum id)).card = 2 ^ A.card := by + have hInjective : + Set.InjOn (fun S ↦ S.sum id) (A.powerset : Set (Finset ℕ)) := by + intro S hS T hT hEqual + exact h S hS T hT hEqual + rw [Finset.card_image_of_injOn hInjective] + exact powersetCardEqTwoPow A + +/-- **Leo Moser's finite variance inequality.** If a finite set of natural +numbers has distinct subset sums, then +`4 ^ |A| - 1 ≤ 3 * ∑ a ∈ A, a ^ 2`. + +This is Theorem 2 of Richard K. Guy's 1982 account, where it is attributed to +Leo Moser. -/ +theorem leoMoserVarianceBound {A : Finset ℕ} + (h : HasDistinctSubsetSums A) : + (4 : ℝ) ^ A.card - 1 ≤ 3 * ∑ a ∈ A, (a : ℝ) ^ 2 := by + set T : Finset ℕ := + A.powerset.image (fun S ↦ S.sum (id : ℕ → ℕ)) with hDefinition + have hCard : T.card = 2 ^ A.card := imageSubsetSumsCard h + have hInjective : + Set.InjOn (fun S ↦ S.sum (id : ℕ → ℕ)) + (A.powerset : Set (Finset ℕ)) := by + intro S hS U hU hEqual + exact h S hS U hU hEqual + have hSumT : + ∑ t ∈ T, (t : ℝ) = + ∑ S ∈ A.powerset, ((S.sum (id : ℕ → ℕ) : ℕ) : ℝ) := by + rw [hDefinition, Finset.sum_image (fun S hS U hU ↦ hInjective hS hU)] + have hSquareSumT : + ∑ t ∈ T, (t : ℝ) ^ 2 = + ∑ S ∈ A.powerset, ((S.sum (id : ℕ → ℕ) : ℕ) : ℝ) ^ 2 := by + rw [hDefinition, Finset.sum_image (fun S hS U hU ↦ hInjective hS hU)] + have hSubsetSumCast : ∀ S : Finset ℕ, + ((S.sum (id : ℕ → ℕ) : ℕ) : ℝ) = ∑ i ∈ S, (i : ℝ) := by + intro S + change ((∑ i ∈ S, id i : ℕ) : ℝ) = ∑ i ∈ S, (i : ℝ) + push_cast + rfl + have hVarianceLower : + (T.card : ℝ) ^ 2 * ((T.card : ℝ) ^ 2 - 1) / 12 ≤ + (T.card : ℝ) * (∑ t ∈ T, (t : ℝ) ^ 2) - + (∑ t ∈ T, (t : ℝ)) ^ 2 := + varianceLowerBoundFinsetNat T + rw [hCard] at hVarianceLower + have hTwoPowCast : + (((2 : ℕ) ^ A.card : ℕ) : ℝ) = (2 : ℝ) ^ A.card := by + push_cast + rfl + rw [hTwoPowCast, hSumT, hSquareSumT] at hVarianceLower + have hSquareSubset : + ∑ S ∈ A.powerset, ((S.sum (id : ℕ → ℕ) : ℕ) : ℝ) ^ 2 = + ∑ S ∈ A.powerset, (∑ i ∈ S, (i : ℝ)) ^ 2 := by + refine Finset.sum_congr rfl (fun S _ ↦ ?_) + rw [hSubsetSumCast] + have hSumSubset : + ∑ S ∈ A.powerset, ((S.sum (id : ℕ → ℕ) : ℕ) : ℝ) = + ∑ S ∈ A.powerset, (∑ i ∈ S, (i : ℝ)) := by + refine Finset.sum_congr rfl (fun S _ ↦ ?_) + rw [hSubsetSumCast] + rw [hSquareSubset, hSumSubset] at hVarianceLower + have hVarianceIdentity := + varianceIdentitySubsetSums A (fun i : ℕ ↦ (i : ℝ)) + have hFirstMoment := sumSubsetSums A (fun i : ℕ ↦ (i : ℝ)) + have hTwoPowPositive : 0 < (2 : ℝ) ^ A.card := by + positivity + have hTwoPowSquarePositive : 0 < ((2 : ℝ) ^ A.card) ^ 2 := by + positivity + have hFourPow : + (4 : ℝ) ^ A.card = ((2 : ℝ) ^ A.card) ^ 2 := by + rw [show (4 : ℝ) = (2 : ℝ) ^ 2 by norm_num, ← pow_mul, mul_comm, pow_mul] + rw [hFourPow] + have hScaledIdentity : + 12 * ((2 : ℝ) ^ A.card * + (∑ U ∈ A.powerset, (∑ i ∈ U, (i : ℝ)) ^ 2) - + (∑ U ∈ A.powerset, (∑ i ∈ U, (i : ℝ))) ^ 2) = + 3 * ((2 : ℝ) ^ A.card) ^ 2 * ∑ a ∈ A, (a : ℝ) ^ 2 := by + have hFirstMomentSquare : + (∑ U ∈ A.powerset, (∑ i ∈ U, (i : ℝ))) ^ 2 * 4 = + ((2 : ℝ) ^ A.card) ^ 2 * (∑ a ∈ A, (a : ℝ)) ^ 2 := by + have hSquare : + (2 * ∑ U ∈ A.powerset, (∑ i ∈ U, (i : ℝ))) ^ 2 = + ((2 : ℝ) ^ A.card * ∑ a ∈ A, (a : ℝ)) ^ 2 := by + rw [hFirstMoment] + nlinarith [hSquare] + nlinarith [hVarianceIdentity, hFirstMomentSquare] + have hScaledBound : + ((2 : ℝ) ^ A.card) ^ 2 * (((2 : ℝ) ^ A.card) ^ 2 - 1) ≤ + 3 * ((2 : ℝ) ^ A.card) ^ 2 * ∑ a ∈ A, (a : ℝ) ^ 2 := by + have hIntermediate : + ((2 : ℝ) ^ A.card) ^ 2 * (((2 : ℝ) ^ A.card) ^ 2 - 1) ≤ + 12 * ((2 : ℝ) ^ A.card * + (∑ U ∈ A.powerset, (∑ i ∈ U, (i : ℝ)) ^ 2) - + (∑ U ∈ A.powerset, (∑ i ∈ U, (i : ℝ))) ^ 2) := by + linarith [hVarianceLower] + linarith [hIntermediate, hScaledIdentity] + nlinarith [hScaledBound, hTwoPowSquarePositive, hTwoPowPositive] + +end LeanPool.ErdosMoser diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 3d96d2dd5a..1997ad95f9 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -5412,3 +5412,57 @@ projects: - "65L06" - "65L05" - "05C05" + - slug: erdos-moser-distinct-subset-sums + title: Leo Moser's finite distinct-subset-sums inequality + summary: >- + Formalizes the exact finite sum-of-squares inequality that Guy's 1982 + account states as Theorem 2 and attributes to Leo Moser: a finite set A + of natural numbers with distinct subset sums satisfies + 4^|A| - 1 <= 3 * sum(a^2). It then derives direct and square-root lower + bounds for the largest element of A. This does not claim the stronger + historical asymptotic bound attributed jointly to Erdős and Moser, and + Erdős Problem 1 remains open. + branch: additive combinatorics + entry_module: LeanPool.ErdosMoser + authors: + - Egor Lyfar + source: + title: Sets of Integers Whose Subsets Have Distinct Sums + authors: + - Richard K. Guy + doi: "10.1016/S0304-0208(08)73500-X" + url: https://www.erdosproblems.com/1 + github_repo: lyfar/lean-pool + license: Apache-2.0 + status: verified + provenance: AI + main_declarations: + - LeanPool.ErdosMoser.leoMoserVarianceBound + main_results: + - declaration: LeanPool.ErdosMoser.leoMoserVarianceBound + informal: >- + If a finite set A of natural numbers has distinct subset sums, then + 4^|A| - 1 is at most three times the sum of the squares of the + elements of A. + source_ref: >- + Richard K. Guy, "Sets of Integers Whose Subsets Have Distinct + Sums," Theorem 2 (credited there to Leo Moser), Annals of Discrete + Mathematics 12 (1982), 141-154, + doi:10.1016/S0304-0208(08)73500-X. + - declaration: LeanPool.ErdosMoser.erdosMoserMaxBound + informal: >- + For a nonempty finite set A of natural numbers with distinct subset + sums, 4^|A| - 1 is at most 3|A| times the square of its largest + element. + - declaration: LeanPool.ErdosMoser.erdosMoserMaxSqrt + informal: >- + The equivalent square-root lower bound on the largest element: + sqrt((4^|A| - 1)/(3|A|)) is at most max(A). + tags: + - additive-combinatorics + - number-theory + - distinct-subset-sums + - erdos-problems + msc: + - "11B13" + - "11B75" From c1ffe9847c2af1939f65521b8e4a0a552f56daa9 Mon Sep 17 00:00:00 2001 From: Egor Lyfar Date: Mon, 27 Jul 2026 22:54:01 +0800 Subject: [PATCH 2/3] =?UTF-8?q?Fix=20Erd=C5=91s-Moser=20project=20metadata?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanPool/ErdosMoser/DiscreteVariance.lean | 1 - LeanPool/projects.yml | 1 - 2 files changed, 2 deletions(-) diff --git a/LeanPool/ErdosMoser/DiscreteVariance.lean b/LeanPool/ErdosMoser/DiscreteVariance.lean index 01119c99e5..e116790aee 100644 --- a/LeanPool/ErdosMoser/DiscreteVariance.lean +++ b/LeanPool/ErdosMoser/DiscreteVariance.lean @@ -6,7 +6,6 @@ Authors: Egor Lyfar import LeanPool.ErdosMoser.Basic import Mathlib.Data.Finset.Sort -import Lean.Elab.Tactic.Omega import Mathlib.Tactic.Linarith import Mathlib.Tactic.Push import Mathlib.Tactic.Ring diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 1997ad95f9..ff9d93e1e2 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -5432,7 +5432,6 @@ projects: - Richard K. Guy doi: "10.1016/S0304-0208(08)73500-X" url: https://www.erdosproblems.com/1 - github_repo: lyfar/lean-pool license: Apache-2.0 status: verified provenance: AI From 437dbd08e4500bc912cb0606d208e385fadb77ae Mon Sep 17 00:00:00 2001 From: Egor Lyfar Date: Mon, 27 Jul 2026 23:21:16 +0800 Subject: [PATCH 3/3] =?UTF-8?q?Link=20Erd=C5=91s-Moser=20companion=20repos?= =?UTF-8?q?itory?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanPool/projects.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index ff9d93e1e2..155a292d32 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -5432,6 +5432,7 @@ projects: - Richard K. Guy doi: "10.1016/S0304-0208(08)73500-X" url: https://www.erdosproblems.com/1 + github_repo: lyfar/erdos-moser-distinct-subset-sums-lean license: Apache-2.0 status: verified provenance: AI