## Stream: Is there code for X?

### Topic: sum_sum_elim for fintypes

#### Oliver Nash (Jul 04 2020 at 16:11):

I'd like to use the fintype-flavour version of the result finset.sum_sum_elim and can't seem to find it. Does it already exist?

#### Oliver Nash (Jul 04 2020 at 16:11):

More precisely, what I would like is hidden.sum_sum_elim:

namespace hidden

open_locale classical
open_locale big_operators

lemma sum_sum_elim
{l m A : Type*} [fintype l] [fintype m] [add_comm_monoid A] (f : l → A) (g : m → A) :
∑ i, sum.elim f g i = (∑ i, f i) + (∑ i, g i) :=
begin
have : @finset.univ (l ⊕ m) _ = finset.image sum.inl finset.univ ∪ finset.image sum.inr finset.univ :=
by { ext a, rcases a; simp, },
by rw [←finset.sum_sum_elim, this],
end

end hidden


#### Jalex Stark (Jul 04 2020 at 16:13):

i thought the point of proving things for finsets is that you can apply them to fintypes and lean will insert the coercion to univ for you

#### Oliver Nash (Jul 04 2020 at 16:14):

Oh I see, that lines up with my surprise at not finding anything for fintypes. Thank you I'll try to proceed along these lines.

#### Oliver Nash (Jul 04 2020 at 16:18):

I wonder if something like the following is missing:

@[simp] lemma finset.univ_sum_union {l m : Type*} [fintype l] [fintype m] :
@finset.univ (l ⊕ m) _ = finset.image sum.inl finset.univ ∪ finset.image sum.inr finset.univ :=
by { ext a, rcases a; simp, }


since we then have:

example {l m : Type*} [fintype l] [fintype m] (f : l → R) (g : m → R) :
∑ i, sum.elim f g i = (∑ i, f i) + (∑ i, g i) :=
by simp


#### Oliver Nash (Jul 04 2020 at 16:34):

(P.S. I love this newish notation for big_operators.)

#### Johan Commelin (Jul 04 2020 at 16:37):

You're welcome :wink:

#### Jalex Stark (Jul 04 2020 at 16:48):

your finset.univ_sum_union looks good to me

#### Jalex Stark (Jul 04 2020 at 16:51):

i'm not sure what file finset.univ_sum_union goes in, but putting that somewhere and sum_sum_elim in big_operators sounds like a fine PR

#### Oliver Nash (Jul 04 2020 at 17:06):

Great. I’ll either include it with some other changes or else make a mini-PR along the lines you suggest.

#### Chris Hughes (Jul 04 2020 at 18:32):

To make this consistent in style with things like sum_sigma and sum_product it would make sense to define the function taking a finset X and a finset Y and returns the disjoint union as a finset (X \oplus Y)

#### Chris Hughes (Jul 04 2020 at 18:42):

This would provide a nicer way to manipulate sums than using sum_union and providing a disjointness proof.

#### Scott Morrison (Jul 05 2020 at 00:18):

I'm not sure that should be a simp lemma.

#### Oliver Nash (Jul 05 2020 at 16:59):

Scott Morrison said:

I'm not sure that should be a simp lemma.

I agree: if anything, it should simplify in the other direction: the disjoint union of two finset.univs is a single finset.univ!

#### Oliver Nash (Jul 05 2020 at 17:01):

I was just looking to pick up this thread again and I discovered that what I was looking for yesterday in fact _does_ exist. It's called fintype.sum_sum_type.

#### Oliver Nash (Jul 05 2020 at 17:07):

I had just started down the road (which I like) that @Chris Hughes had sketched out, which I interpreted as something like:

variables {α γ : Type*}

def disjoint_union (s : finset α) (t : finset γ) : finset (α ⊕ γ) :=
s.image sum.inl ∪ t.image sum.inr

def finset.sum_proj_l (s : finset (α ⊕ γ)) : (finset α) := sorry

def finset.sum_proj_r (s : finset (α ⊕ γ)) : (finset γ) := sorry

lemma finset.proj_l_disjoint_union (s : finset α) (t : finset γ) :
s = (disjoint_union s t).sum_proj_l := sorry

lemma finset.proj_r_disjoint_union (s : finset α) (t : finset γ) :
t = (disjoint_union s t).sum_proj_r := sorry

lemma finset.disjoint_union_proj_lr (s : finset (α ⊕ γ)) :
s = disjoint_union s.sum_proj_l s.sum_proj_r := sorry

def finset.sum_equiv' : finset (α ⊕ γ) ≃ (finset α) × (finset γ) := sorry

-- The lemma I originally wanted, so that I could use finset.sum_sum_elim:
@[simp] lemma finset.disjoint_union_univ {l m : Type*} [fintype l] [fintype m] :
disjoint_union finset.univ finset.univ = @finset.univ (l ⊕ m) _ :=
by { ext a, rcases a; simp [disjoint_union], }


but having found fintype.sum_sum_type I'm going to park all this, even if the existence of fintype.sum_sum_type does seem a bit inconsistent with the philosophy outlined by @Jalex Stark

Last updated: May 07 2021 at 21:10 UTC