Finset sum bounds

Stream: Is there code for X?

[Jeremy Tan]

Do these four lemmas already exist in mathlib, and can they be proved simpler?

/-
Copyright (c) 2025 Jeremy Tan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Tan
-/
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Int.Interval

/-!
# Sharp bounds for sums of bounded finsets of integers

The sum of a finset of integers with cardinality `s` where all elements are at most `c` can be given
a sharper upper bound than `#s * c`, because the elements are distinct.

This file provides these sharp bounds, both in the upper-bounded and analogous lower-bounded cases.
-/


namespace Finset

/-- Sharp upper bound for the sum of a finset of integers that is bounded above, `Ioc` version. -/
lemma sum_le_sum_Ioc {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, x ≤ c) :
    ∑ x ∈ s, x ≤ ∑ x ∈ Ioc (c - #s) c, x := by
  set r := Ioc (c - #s) c
  calc
    _ ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - #s) := by
      rw [← sum_inter_add_sum_diff s r _]
      refine add_le_add_left (sum_le_card_nsmul _ _ _ fun x mx ↦ ?_) _
      rw [mem_sdiff, mem_Ioc, not_and'] at mx
      have := mx.2 (hs _ mx.1); omega
    _ = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - #s) := by
      rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ioc, sub_sub_cancel, Int.toNat_ofNat]
    _ ≤ _ := by
      rw [← sum_inter_add_sum_diff r s _]
      refine add_le_add_left (card_nsmul_le_sum _ _ _ fun x mx ↦ ?_) _
      rw [mem_sdiff, mem_Ioc] at mx; exact mx.1.1.le

/-- Sharp upper bound for the sum of a finset of integers that is bounded above, `range` version. -/
lemma sum_le_sum_range {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, x ≤ c) :
    ∑ x ∈ s, x ≤ ∑ n ∈ range #s, (c - n) := by
  convert sum_le_sum_Ioc hs
  refine sum_nbij (c - ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)
  · intro x mx; rw [mem_Ioc]; dsimp only; rw [mem_range] at mx; omega
  · intro x mx y my (h : c - x = c - y); omega
  · intro x mx; simp_rw [coe_range, Set.mem_image, Set.mem_Iio]
    rw [mem_coe, mem_Ioc] at mx
    use (c - x).toNat; omega

/-- Sharp lower bound for the sum of a finset of integers that is bounded below, `Ico` version. -/
lemma sum_Ico_le_sum {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, c ≤ x) :
    ∑ x ∈ Ico c (c + #s), x ≤ ∑ x ∈ s, x := by
  set r := Ico c (c + #s)
  calc
    _ ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + #s) := by
      rw [← sum_inter_add_sum_diff r s _]
      refine add_le_add_left (sum_le_card_nsmul _ _ _ fun x mx ↦ ?_) _
      rw [mem_sdiff, mem_Ico] at mx; exact mx.1.2.le
    _ = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + #s) := by
      rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_ofNat]
    _ ≤ _ := by
      rw [← sum_inter_add_sum_diff s r _]
      refine add_le_add_left (card_nsmul_le_sum _ _ _ fun x mx ↦ ?_) _
      rw [mem_sdiff, mem_Ico, not_and] at mx
      have := mx.2 (hs _ mx.1); omega

/-- Sharp lower bound for the sum of a finset of integers that is bounded below, `range` version. -/
lemma sum_range_le_sum {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, c ≤ x) :
    ∑ n ∈ range #s, (c + n) ≤ ∑ x ∈ s, x := by
  convert sum_Ico_le_sum hs
  refine sum_nbij (c + ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)
  · intro x mx; rw [mem_Ico]; dsimp only; rw [mem_range] at mx; omega
  · intro x mx y my (h : c + x = c + y); omega
  · intro x mx; simp_rw [coe_range, Set.mem_image, Set.mem_Iio]
    rw [mem_coe, mem_Ico] at mx
    use (x - c).toNat; omega

end Finset

[Jeremy Tan]

They came out of my formalisation of IMO 2015 Q6

[Jeremy Tan]

#23038

[Eric Wieser]

I would guess these generalize to any locally finite linear order?

[Jeremy Tan]

Eric Wieser said:

I would guess these generalize to any locally finite linear order?

ℤ and ℕ are the only explicit locally finite linear orders I can think of; I can't think of the right way to modify Ioc (c - #s) c for arbitrary locally finite linear orders

[Jeremy Tan]

Is it true that any locally finite linear order admits an order homomorphism into the integers?

[Jeremy Tan]

(Really though, I am also taking a sum over the elements of the finset, so I certainly need more than just a locally finite linear order)

[Bhavik Mehta]

What about this: if f is a monotone map from a locally finite order to a linearly ordered add comm monoid, for any s, Finset.sum s f is <= Finset.sum t f where t is an upper set of the same cardinality as s. More generally, if s is upper bounded below c then t is an upper set below c of the same cardinality. (To be clear, I mean forall s, there exists t, ...)

[Jeremy Tan]

So like this?

namespace Finset

variable {α : Type*} [Preorder α] [LocallyFiniteOrder α]
  {β : Type*} [LinearOrder β] [AddCommMonoid β]

lemma xxx {f : α → β} (hf : Monotone f) {s : Finset α} {c : α} (hs : ↑s ⊆ Set.Iic c) :
    ∃ t : Finset (Set.Iic c), IsUpperSet t.toSet ∧ #s = #t ∧
      s.sum f ≤ (t.map (Function.Embedding.subtype _)).sum f := by
  sorry

[Bhavik Mehta]

Something like this, yes, although I'd prefer the condition of t being an upper set relative to c being stated in a way which doesn't involve subtypes; it seems like we don't have an existing def for this though :/

[Jeremy Tan]

@Bhavik Mehta does this look like a good definition?

/-- A bounded upper set in an order `α` relative to `c : α` is a set such that all elements are
less than `c` and any element greater than one of its members and less than `c` is also a member. -/
def IsBoundedUpperSet {α : Type*} [LE α] (s : Set α) (c : α) : Prop :=
  ∀ ⦃a : α⦄, a ∈ s → a ≤ c ∧ ∀ ⦃b : α⦄, a ≤ b → b ∈ s

/-- A bounded lower set in an order `α` relative to `c : α` is a set such that all elements are
greater than `c` and any element less than one of its members and greater than `c` is also
a member. -/
def IsBoundedLowerSet {α : Type*} [LE α] (s : Set α) (c : α) : Prop :=
  ∀ ⦃a : α⦄, a ∈ s → c ≤ a ∧ ∀ ⦃b : α⦄, b ≤ a → b ∈ s

[Jeremy Tan]

Bhavik Mehta said:

Something like this, yes, although I'd prefer the condition of t being an upper set relative to c being stated in a way which doesn't involve subtypes; it seems like we don't have an existing def for this though :/

I've opened #23762 to define relative upper and lower sets. Now the lemma xxx would be stated as

namespace Finset

variable {α : Type*} [Preorder α] [LocallyFiniteOrder α]
  {β : Type*} [LinearOrder β] [AddCommMonoid β]

lemma xxx {f : α → β} (hf : Monotone f) {s : Finset α} {c : α} (hs : ∀ x ∈ s, x ≤ c) :
    ∃ t : Finset α, IsRelUpperSet t c ∧ #s = #t ∧ s.sum f ≤ t.sum f := by
  sorry