linear combination is in span

Stream: Is there code for X?

[Vasily Ilin]

It seems that this should be an existing theorem but I can't find it. docs#mem_span_finset seems relevant but I'm not sure how to use it, since I don't have a finset but set.range v instead.

import tactic
import linear_algebra.basis
import data.real.basic
import data.complex.basic
import data.complex.module
import data.matrix.notation

open_locale big_operators

example (n : ℕ) (w : V) (v : fin n → V) (coeff : fin n → k) (w = ∑ i : fin n, (coeff i • v i)) : w ∈ submodule.span k (set.range v) :=

[Eric Wieser]

That ought to be straightforward via rw H, apply sum_mem, intro i, apply subset_span

[Eric Wieser]

docs#submodule.subset_span

[Nikolas Kuhn]

One could even make this into an if and only if :)

[Eric Wieser]

What statement are you thinking of?

[Nikolas Kuhn]

There are mem_span_iff_total and span_image_eq_map_total in docs#linear_algebra.finsupp which should pretty much do the job.

[Jon Eugster]

To take this up again, does anybody know some nice code to express an element in span as some sort of sum ? For example something like

lemma mem_span_iff_sum_coeff {v : V} {n : ℕ} {b : fin n → V} :
  v ∈ span R (set.range b) ↔ ∃ (coef : fin n → R), v = ∑ i, (coef i) • (b i) :=
sorry

MWE preample

import algebra.module.submodule.lattice
import data.real.basic            -- definiert `ℝ`
import algebra.module.pi          -- definiert `module ℚ (fin 2 → ℚ)`
import data.matrix.notation       -- Importiert Matrix/Vektor-Notation
import data.finset
import linear_algebra.finsupp
import algebra.big_operators.default
import algebra.big_operators.finprod

open_locale big_operators
open submodule

variables {R V : Type*} [ring R] [add_comm_monoid V] [module R V]

Backwards direction is okay (as above, although I don't get @Eric Wieser 's suggestion with sum_mem to work), but in the forward direction I'm getting hung up on different finiteness options (fin n → vs →₀, ∑ vs ∑ᶠ vs finsupp.total and similar stuff)

The main application for me is to show that some sets of vectors are generating a vector space (maybe there's a better way to do that, too?) :

example : ⊤ ≤ span ℝ (set.range ![![(1: ℝ), 0], ![1, 1]]) :=
begin
  intros v hv,
  rw mem_span_iff_sum_coeff,
  use ![v 0 - v 1, v 1],
  simp,
  funext i,
  fin_cases i;
  simp,
end

[Jujian Zhang]

Try span.repr https://leanprover-community.github.io/mathlib_docs/linear_algebra/finsupp.html#span.repr

[Jujian Zhang]

or maybe submodule.mem_span_finset https://leanprover-community.github.io/mathlib_docs/linear_algebra/finsupp.html#mem_span_finset

[Eric Wieser]

I would guess that you want to use docs#submodule.span_range_eq_supr

[Jon Eugster]

Thanks for the help, both of you! I ended up using mainly mem_span_iff_total, and with a bit more knowledge of how fin n and finset play together (which I don't have), your suggestions seem very useful, too.

MWE

import algebra.module.submodule.lattice
import data.real.basic
import algebra.module.pi
import data.matrix.notation
import linear_algebra.finsupp
import algebra.big_operators.default

open_locale big_operators
open submodule

variables {R V : Type*} [ring R] [add_comm_monoid V] [module R V]
variables {v : V} {n : ℕ} {b : fin n → V}

lemma mem_span_iff_sum_coeff :
  v ∈ span R (b '' set.univ) ↔ ∃ (coef : fin n →₀ R), v = ∑ i, (coef i) • (b i) :=
begin
  constructor,
  { rw finsupp.mem_span_image_iff_total R,
    intro h,
    rcases h with ⟨coef, h₁, h₂⟩,
    use coef,
    rw ←h₂,
    rw finsupp.total_apply,
    apply finsupp.sum_fintype,
    simp },
  { rw finsupp.mem_span_image_iff_total R,
    intro h,
    cases h with coef h,

    -- put `lift coef to fin n →₀ R using ⟨fintype.of_finite ↥(function.support coef)⟩,`
    -- here to use `(coef : fin n → R)` in the statement.

    use coef,
    constructor,
    { simp },
    { rw h,
      rw finsupp.total_apply,
      apply finsupp.sum_fintype,
      simp }}
end

[Eric Wieser]

docs#finsupp.range_total seems to be the really useful lemma here