Get smallest k elements of a Set of natural numbers

Stream: new members

[Riley Riles]

Is there a good way to get a Finset that consists of the smallest k elements of a Set of natural numbers?

[Jireh Loreaux]

Is your set infinite? How do you know it has k elements?

[Riley Riles]

Suppose I can prove the set is infinite, yes.

[Jireh Loreaux]

I would probably go with docs#Finset.range, docs#Finset.map, docs#Nat.nth with the predicate p being (· ∈ s).

[Riley Riles]

Gotcha, thanks!

[Sabbir Rahman]

One can also do following I guess

import Mathlib

noncomputable def smallest_n_finset (s : Set ℕ) (n : ℕ) : Finset ℕ  :=
  ((List.range n).map (fun k ↦ Nat.nth s k)).toFinset

But this will not behave as expected when size of s is smaller than n.

[Riley Riles]

After looking into this, this does seem somewhat tricky to work with—I would like to eventually prove that the product of the smallest n elements of any infinite set of natural numbers is smaller than the product of any other n elements in the same set, but this definition is quite difficult to use for such a proof. I don't suppose there're any pre-existing theorems on the topic? I tried searching the docs/Loogle/Moogle but could not find anything.

[Kevin Buzzard]

(nit: it's not always strictly smaller if n>=1 and the set contains 0)

[Riley Riles]

Right, I will assume that I can prove that this set does not contain zero. (Apologies for the omission; I am still new to using Zulip.)

[Yakov Pechersky]

Not exactly the right proof, there's some juggle of the minimum element of the set on the right. But a start:

import Mathlib

noncomputable def smallest_n_finset (s : Set ℕ) (n : ℕ) : Finset ℕ  :=
  ((Finset.range n).image (fun k ↦ Nat.nth (· ∈ s) k))

lemma card_smallest_n_finset {s : Set ℕ} (hs : s.Infinite) (n : ℕ) :
    (smallest_n_finset s n).card = n := by
  rw [smallest_n_finset, Finset.card_image_of_injective, Finset.card_range]
  exact (Nat.nth_strictMono hs).injective

@[simp]
lemma smallest_n_finset_zero (s : Set ℕ)  :
    smallest_n_finset s 0 = ∅ := by
  rfl

lemma nth_mem_not_in_smallest_n_finset_of_le {s : Set ℕ} (hs : s.Infinite) {n k : ℕ} (h : n ≤ k) :
    Nat.nth (· ∈ s) k ∉ smallest_n_finset s n := by
  rw [smallest_n_finset, Finset.mem_image]
  simp only [Finset.mem_range, not_exists, not_and]
  intro l hl H
  exact (hl.trans_le h).ne ((Nat.nth_strictMono hs).injective H)

lemma smallest_n_finset_succ {s : Set ℕ} (hs : s.Infinite) (n : ℕ) :
    smallest_n_finset s (n + 1) = (smallest_n_finset s n).cons (Nat.nth (· ∈ s) n)
      (nth_mem_not_in_smallest_n_finset_of_le hs le_rfl) := by
  simp [smallest_n_finset, Finset.range_succ, Finset.image_insert]

example (s : Set ℕ) (hs : s.Infinite) (hs0 : 0 ∉ s) (n : ℕ)
    (t : Finset ℕ) (ht : (t : Set ℕ) ⊆ s) (ht' : n ≤ t.card) :
    (smallest_n_finset s n).prod id ≤ t.prod id := by
  induction t using Finset.cons_induction_on generalizing n with
  | h₁ =>
    simp only [Finset.card_empty, nonpos_iff_eq_zero] at ht'
    simp [ht']
  | @h₂ a t ha IH =>
    simp only [Finset.cons_eq_insert, Finset.coe_insert, ha, not_false_eq_true,
      Finset.card_insert_of_not_mem, id_eq, Finset.prod_insert] at ht ht' ⊢
    have hts := ((Set.subset_insert _ _).trans ht)
    rcases ht'.eq_or_lt with ht'|ht'
    · obtain ⟨b, hb, hb'⟩ : ∃ b ∈ (insert a t), ∀ c ∈ (insert a t), b ≤ c := by
        refine ⟨Finset.min' (insert a t) ?_, ?_, ?_⟩
        · simp [ha]
        · exact Finset.min'_mem _ _
        · intro c hc
          exact Finset.min'_le _ _ hc
      rw [ht', smallest_n_finset_succ hs, Finset.prod_cons]
      refine Nat.mul_le_mul ?_ ?_
      · sorry
      · exact IH _ hts _
    · refine (IH n hts (Nat.le_of_lt_succ ht')).trans ?_
      exact le_mul_of_one_le_left _ _

[Jireh Loreaux]

I wonder if using docs#Finset.induction_on_min (or docs#Finset.induction_on_max) makes that juggling any easier.