sum_sum_elim for fintypes

Stream: Is there code for X?

[Oliver Nash]

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]

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]

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]

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]

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]

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

[Johan Commelin]

You're welcome :wink:

[Jalex Stark]

your finset.univ_sum_union looks good to me

[Jalex Stark]

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]

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

[Chris Hughes]

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]

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

[Scott Morrison]

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

[Oliver Nash]

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]

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]

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