# Zulip Chat Archive

## 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 2*d possibilities), and the other (d-1) can take any value ((2*m+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