## Stream: new members

### Topic: bounding finset.filter

#### Eloi (Jul 21 2020 at 10:55):

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 (Jul 21 2020 at 12:53):

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 (Jul 21 2020 at 12:55):

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

#### Scott Morrison (Jul 21 2020 at 12:56):

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

#### Eloi (Jul 21 2020 at 12:56):

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

#### Kevin Buzzard (Jul 21 2020 at 12:58):

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 (Jul 21 2020 at 13:01):

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

#### Scott Morrison (Jul 21 2020 at 13:02):

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

#### Scott Morrison (Jul 21 2020 at 13:02):

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 (Jul 21 2020 at 13:03):

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

#### Eloi (Jul 21 2020 at 13:05):

Thanks! I will give it a try :)

#### Eloi (Jul 21 2020 at 15:37):

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 (Jul 21 2020 at 17:36):

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

#### Eloi (Jul 21 2020 at 18:09):

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 (Jul 22 2020 at 00:30):

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 (Jul 22 2020 at 00:35):

This kind of union exists as finset.bind

#### Alistair Tucker (Jul 22 2020 at 00:38):

So it does :smile: Better use bind then.

Last updated: May 10 2021 at 23:11 UTC