Sum is in span

Stream: Is there code for X?

[Nikolas Kuhn]

Do we have that if a number of elements is in a set s, then their sum is in the span? (Coincidentally, this was also just asked for linear combinations here ). If not, maybe it'd be worth adding? I'm envisioning something like this:

import linear_algebra.span
import logic.equiv.fin

lemma mem_span_of_sum (R M : Type) (s : set M) (d : ℕ) (m : fin d → M) (hm : set.range m ⊆ s)
  [comm_ring R] [add_comm_monoid M] [module R M] : (∑ i, m i ∈ submodule.span R s) :=
begin
  induction d with k hk,
  { rw [fintype.sum_equiv fin_zero_equiv],
    { rw [fintype.sum_empty],
      exact submodule.zero_mem _, },
    { exact fin_zero_elim, exact empty.elim, }, },
  rw [← equiv.sum_comp (fin_succ_equiv k).symm m, fintype.sum_option],
  refine submodule.add_mem _ _ _,
  { simp only [fin_succ_equiv_symm_none],
    have := (set.mem_of_subset_of_mem hm (set.mem_range_self (0 : fin k.succ))),
    exact set_like.mem_coe.mp (set.mem_of_subset_of_mem submodule.subset_span this), },
  apply hk,
  simp only [fin_succ_equiv_symm_some],
  apply set.subset.trans _ hm,
  exact set.range_comp_subset_range (λ (x : fin k), x.succ) m,
end

Of course, one might also allow maps from an arbitrary finite type etc.

[Yakov Pechersky]

It would be simpler to prove if stated more generally instead of a sum over a fintype used for indexing, you used sum over a finset

[Eric Wieser]

It follows trivially from docs#sum_mem, doesn't it?

[Yakov Pechersky]

import linear_algebra.span

open_locale big_operators

lemma mem_span_of_sum (R M ι : Type*) [comm_ring R] [add_comm_monoid M] [module R M]
  (s : set M) (t : finset ι) (f : ι → M) (hm : (t : set ι) ⊆ f ⁻¹' s) :
  ∑ i in t, f i ∈ submodule.span R s :=
begin
  refine sum_mem _,
  intros x hx,
  rw submodule.mem_span,
  intros p hp,
  rw ←set.image_subset_iff at hm,
  exact hm.trans hp ⟨x, hx, rfl⟩
end

lemma mem_span_of_sum' (R M : Type) (s : set M) (d : ℕ) (m : fin d → M) (hm : set.range m ⊆ s)
  [comm_ring R] [add_comm_monoid M] [module R M] : (∑ i, m i ∈ submodule.span R s) :=
begin
  refine mem_span_of_sum _ _ _ _ _ _ _,
  simpa [←set.image_subset_iff] using hm
end

[Nikolas Kuhn]

Eric Wieser said:

It follows trivially from docs#sum_mem, doesn't it?

Ah, great! Somehow I missed that.

[Nikolas Kuhn]

I like your solution, Yakov! Maybe you could think making it a PR? (I'm still new, so you can probably better judge whether you think it's suitable)

[Yakov Pechersky]

Since you're new, you making a PR on this would be a great way to get familiar with the process.

[Eric Wieser]

I'm not convinced either lemma is really worth having vs just using the existing API. Does using docs#submodule.subset_span make the first proof even shorter?

[Nikolas Kuhn]

Using the suggestion, I got the first one down to

lemma mem_span_of_sum (R M ι : Type*) [comm_ring R] [add_comm_monoid M] [module R M]
  (s : set M) (t : finset ι) (f : ι → M) (hm : f '' t ⊆ s) :
  ∑ i in t, f i ∈ submodule.span R s :=
begin
  refine sum_mem _,
  intros x hx,
  apply set.mem_of_mem_of_subset _ submodule.subset_span,
  exact set.mem_of_mem_of_subset (set.mem_image_of_mem f hx) hm,
end

(note the change to (hm : f '' t ⊆ s) in the hyothesis, I'm not sure either one is better).
I agree that this is probably too close to sum_mem to be worth it, but I find the version using a sum over a fintype the most natural, so it might be nice to have it.

[Eric Wieser]

I think apply subset_span directly would work after the intros?

[Nikolas Kuhn]

It does! So apply knows about set.mem_of_mem_of subset?!

[Eric Wieser]

Have a look at how src#set.mem_of_mem_of_subset is proved

[Nikolas Kuhn]

Those are very good hints:

lemma mem_span_of_sum (R M ι : Type*) [comm_ring R] [add_comm_monoid M] [module R M]
  (s : set M) (t : finset ι) (f : ι → M) (hm : f '' t ⊆ s) :
  ∑ i in t, f i ∈ submodule.span R s :=
  sum_mem (λ x hx, submodule.subset_span (hf (set.mem_image_of_mem f hx)))

[Nikolas Kuhn]

And by taking the same proof term, you can make the other version a one-liner, too (not depending on this one):

lemma mem_span_of_sum' (R : Type*) {M : Type*} {s : set M} {d : ℕ} (f : fin d → M) (hf : set.range f ⊆ s)
  [comm_ring R] [add_comm_monoid M] [module R M] :
  (∑ i, f i ∈ submodule.span R s) :=
  sum_mem (λ x hx, submodule.subset_span  $ hf $ set.mem_range_self x)

I see what you mean now.