Lists as finsupp #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

list.to_finsupp: Interpret a list as a finitely supported function, where the indexing type is ℕ, and the values are either the elements of the list (accessing by indexing) or 0 outside of the list.

Main theorems #

list.to_finsupp_eq_sum_map_enum_single: A l : list M over M an add_monoid, when interpreted as a finitely supported function, is equal to the sum of finsupp.single produced by mapping over list.enum l.

Implementation details #

The functions defined here rely on a decidability predicate that each element in the list can be decidably determined to be not equal to zero or that one can decide one is out of the bounds of a list. For concretely defined lists that are made up of elements of decidable terms, this holds. More work will be needed to support lists over non-dec-eq types like ℝ, where the elements are beyond the dec-eq terms of casted values from ℕ, ℤ, ℚ.

source

def list.to_finsupp {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ℕ), l.nthd i 0 ≠ 0)] :

ℕ →₀ M

Indexing into a l : list M, as a finitely-supported function, where the support are all the indices within the length of the list that index to a non-zero value. Indices beyond the end of the list are sent to 0.

This is a computable version of the finsupp.on_finset construction.

Equations

l.to_finsupp = {support := finset.filter (λ (i : ℕ), l.nthd i 0 ≠ 0) (finset.range l.length), to_fun := λ (i : ℕ), l.nthd i 0, mem_support_to_fun := _}

source

@[norm_cast]

theorem list.coe_to_finsupp {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ℕ), l.nthd i 0 ≠ 0)] :

⇑(l.to_finsupp) = λ (i : ℕ), l.nthd i 0

source

@[simp, norm_cast]

theorem list.to_finsupp_apply {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ℕ), l.nthd i 0 ≠ 0)] (i : ℕ) :

⇑(l.to_finsupp) i = l.nthd i 0

source

theorem list.to_finsupp_support {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ℕ), l.nthd i 0 ≠ 0)] :

l.to_finsupp.support = finset.filter (λ (i : ℕ), l.nthd i 0 ≠ 0) (finset.range l.length)

source

theorem list.to_finsupp_apply_lt {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ℕ), l.nthd i 0 ≠ 0)] (n : ℕ) (hn : n < l.length) :

⇑(l.to_finsupp) n = l.nth_le n hn

source

theorem list.to_finsupp_apply_le {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ℕ), l.nthd i 0 ≠ 0)] (n : ℕ) (hn : l.length ≤ n) :

⇑(l.to_finsupp) n = 0

source

@[simp]

theorem list.to_finsupp_nil {M : Type u_1} [has_zero M] [decidable_pred (λ (i : ℕ), list.nil.nthd i 0 ≠ 0)] :

list.nil.to_finsupp = 0

source

theorem list.to_finsupp_singleton {M : Type u_1} [has_zero M] (x : M) [decidable_pred (λ (i : ℕ), [x].nthd i 0 ≠ 0)] :

[x].to_finsupp = finsupp.single 0 x

source

@[simp]

theorem list.to_finsupp_cons_apply_zero {M : Type u_1} [has_zero M] (x : M) (xs : list M) [decidable_pred (λ (i : ℕ), (x :: xs).nthd i 0 ≠ 0)] :

⇑((x :: xs).to_finsupp) 0 = x

source

@[simp]

theorem list.to_finsupp_cons_apply_succ {M : Type u_1} [has_zero M] (x : M) (xs : list M) (n : ℕ) [decidable_pred (λ (i : ℕ), (x :: xs).nthd i 0 ≠ 0)] [decidable_pred (λ (i : ℕ), xs.nthd i 0 ≠ 0)] :

⇑((x :: xs).to_finsupp) n.succ = ⇑(xs.to_finsupp) n

source

theorem list.to_finsupp_cons_eq_single_add_emb_domain {R : Type u_1} [add_zero_class R] (x : R) (xs : list R) [decidable_pred (λ (i : ℕ), (x :: xs).nthd i 0 ≠ 0)] [decidable_pred (λ (i : ℕ), xs.nthd i 0 ≠ 0)] :

(x :: xs).to_finsupp = finsupp.single 0 x + finsupp.emb_domain {to_fun := nat.succ, inj' := nat.succ_injective} xs.to_finsupp

source

theorem list.to_finsupp_concat_eq_to_finsupp_add_single {R : Type u_1} [add_zero_class R] (x : R) (xs : list R) [decidable_pred (λ (i : ℕ), (xs ++ [x]).nthd i 0 ≠ 0)] [decidable_pred (λ (i : ℕ), xs.nthd i 0 ≠ 0)] :

(xs ++ [x]).to_finsupp = xs.to_finsupp + finsupp.single xs.length x

source

theorem list.to_finsupp_eq_sum_map_enum_single {R : Type u_1} [add_monoid R] (l : list R) [decidable_pred (λ (i : ℕ), l.nthd i 0 ≠ 0)] :

l.to_finsupp = (list.map (λ (nr : ℕ × R), finsupp.single nr.fst nr.snd) l.enum).sum