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