bounding finset.filter

Stream: new members

[Eloi]

Hi, I want to bound the cardinal of a finset generated with finset.filter. I have two lemmas, and the proof of the first one is easy: we choose the coordinate that satisfies the proposition (there are 2d possibilities), and the other (d-1) can take any value ((2m+1)^(d-1) possibilities). How can I make progress to write this proof in lean?

import tactic
import data.fintype.basic
import data.finset.basic

/--
  For each integer N, we define the set
      `{ n ∈ ℤᵈ   | max(n₁, ..., n_d) ≤ N }`
-/
definition S' (N: ℕ ) (d: ℕ) : finset (fin d → ℤ) :=
  fintype.pi_finset (λ a, finset.Ico_ℤ (- N) (N+1))

/--
  For each integer N, we define the set
      `{n | ∀ i, (n i).nat_abs ≤ m  ∧ ∃ (i : fin d), n i = m}`
-/
definition S (N: ℕ ) (d: ℕ) : finset (fin d → ℤ) :=
    finset.filter (λ n, ∃ (i : fin d), n i = N) (S' N d)

lemma easy_S_card_le (m: ℕ)(d: ℕ) :  (S m d).card ≤ 2 * d * (2 * m + 1) ^ (d -1) :=
begin
  unfold S S',
  sorry,
end

And this is the second lemma that I'll attempt after I manage to prove the first.

lemma S_card_le (m: ℕ)(d: ℕ) :  (S m d).card ≤ d * (2 * m + 1) ^ (d -1) :=
begin
  unfold S S',
  sorry,
end
-- Check that the previous lemma holds for small values.
--#eval (list.iota 5).map (λ m, (list.iota 5).map (λ d,(S m d).card - d * (2 * m + 1) ^ (d-1)))

[Kevin Buzzard]

This looks like the kind of thing that ends up on proof grounds and is really nasty to do in lean, there are people around who are good at this type of question but I'm pretty sure it would take me an age to do

[Scott Morrison]

The specification comment of your definition S' doesn't match the implementation.

[Scott Morrison]

(The comment indicates an infinite set, with unboundedly negative entries allowed.)

[Eloi]

Sorry, It is max( |a_1|, ..., |a_d|)

[Kevin Buzzard]

If someone put a gun to my head I would try to prove that fin (succ d) -> Z was the product of fin d -> Z and Z, show that the corresponding filter was an "or", prove that filtering on P or Q gave me at most as many elements as summing the sizes of filtering on P and on Q etc etc etc.

[Scott Morrison]

Show the set is the (non-disjoint) union over the sets where the i-th coordinate has absolute value N.

[Scott Morrison]

In each of those sets, that i-th coordinate is either -N or N.

[Scott Morrison]

In each of those sets, the filter condition is trivial (because it's implied by the extra condition), so you just need to count the size of S'.

[Scott Morrison]

No inductions, in particular, they are going to be horrible.

[Eloi]

Thanks! I will give it a try :)

[Eloi]

Scott Morrison said:

Show the set is the (non-disjoint) union over the sets where the i-th coordinate has absolute value N.

I figured out how to prove that S is this union, but for sets and not finsets :(, can anyone help me to translate the statement S_is_union_of_S_aux_i to finsets? In particular I don't know how to do a union over finsets.

import tactic
import data.fintype.basic
import data.finset.basic

/--
  For each integer N, we define the set
      `{ n ∈ ℤᵈ   | max(n₁, ..., n_d) ≤ N }`
-/
definition S' (N: ℕ ) (d: ℕ) : finset (fin d → ℤ) :=
  fintype.pi_finset (λ a, finset.Ico_ℤ (- N) (N+1))

/--
  For each integer N, we define the set
      `{ n ∈ ℤᵈ   | max(|n₁|, ..., |n_d|) ≤ N }`
      `{n  ∈ ℤᵈ   | ∀ i, (n i).nat_abs ≤ m  ∧ ∃ (i : fin d), |n i| = m}`
-/
definition S (N: ℕ ) (d: ℕ) : finset (fin d → ℤ) :=
    finset.filter (λ n, ∃ (i : fin d), (n i).nat_abs = N) (S' N d)


/--
  This is the auxiliary set
      `{n ∈ ℤᵈ |   max(|n₁|, ..., |n_d|) ∧ |n i| = m }`
-/
definition S_aux (N: ℕ)(d:ℕ)(i: fin d): finset (fin d → ℤ) :=
  finset.filter (λ n, (n i).nat_abs = N) (S' N d)

lemma S_is_union_of_S_aux_i (N: ℕ)(d: ℕ) : (↑(S N d): set (fin d → ℤ)) =  ⋃ i : fin d , ↑(S_aux N d i):=
  begin
    ext1,
    split,
    {intro hx,
    norm_num at *,
    unfold S at *,
    simp at *,
    cases hx,
    unfold S_aux,
    use classical.some hx_right,
    simp,
    exact ⟨hx_left, classical.some_spec hx_right⟩,
    },
    intro hx,
    unfold S_aux at *,
    unfold S,
    simp at *,
    exact hx,
  end


lemma S_card_le (m: ℕ)(d: ℕ) :  (S m d).card ≤ 2 * d * (2 * m + 1) ^ (d -1) :=
begin
  unfold S S',
  sorry,
end

[Alistair Tucker]

To take the union you can write finset.sup finset.univ (λ i, S_aux N d i)

[Eloi]

Thanks! Maybe this could have some union notation in order to be easier...

Now I have the problem that simp does not simplify this union, wereas before it worked.

lemma S_is_union' (N: ℕ)(d: ℕ) : S N d =  finset.sup finset.univ (λ i, S_aux N d i):=
  begin
    ext1,
    split,
    {intro hx,
    norm_num at *,
    unfold S at *,
    simp at hx,
    cases hx,
    cases hx_right,
    --unfold S_aux, -- does not "see" the S_aux inside the union.

    --use hx_right_w, -- doesn't work

    hint, --not useful

    --simp,
   -- exact ⟨hx_left,  hx_right⟩,
    sorry,
    },
    intro hx,
    unfold S_aux at *,
    unfold S,
    simp at *, -- simp does not simplify hx,
    -- hx: a ∈ finset.univ.sup (λ (i : fin d), finset.filter (λ (n : fin d → ℤ), (n i).nat_abs = N) (S' N d))
    sorry,  --exact hx,
  end

[Alistair Tucker]

I think you need that something is in a union of sets if and only if it is in one of the sets. For set itself that's not a problem, the lemma is already in mathlib and is marked with @[simp] so the tactic can use it. But for finset I can't find it at all. Doesn't mean it's not in there somewhere! and if it is it'll have a much nicer proof than this one:

lemma mem_sup_iff (α β : Type) [decidable_eq α] [decidable_eq β] (f : α → finset β)
    (t : finset α) (b : β) : b ∈ t.sup f ↔ ∃ a ∈ t, b ∈ f a :=
begin
  apply finset.induction_on t,
  { rw finset.sup_empty,
    split,
    { apply false.elim, },
    { rintros ⟨a, ha, hb⟩,
      exact false.elim ha, }, },
  intros a' s h' ih,
  rw [finset.sup_insert, finset.sup_eq_union, finset.mem_union],
  split,
  { intro h,
    cases h with h₁ h₂,
    { exact ⟨a', finset.mem_insert_self a' s, h₁⟩, },
    { rcases ih.1 h₂ with ⟨a, ha, hb⟩,
      exact ⟨a, finset.mem_insert_of_mem ha, hb⟩, }, },
  { rintros ⟨a, ha, hb⟩,
    cases finset.mem_insert.1 ha,
    { rw h at hb,
      exact or.inl hb, },
    { exact or.inr (ih.2 ⟨a, h, hb⟩), }, },
end

[Reid Barton]

This kind of union exists as finset.bind

[Alistair Tucker]

So it does :smile: Better use bind then.