# Documentation

Mathlib.Data.List.ToFinsupp

# Lists as finsupp #

## Main definitions #

• List.toFinsupp: 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.toFinsupp_eq_sum_map_enum_single: A l : List M over M an AddMonoid, 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 ℕ, ℤ, ℚ.

def List.toFinsupp {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => List.getD l x 0 0] :

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.onFinset construction.

Instances For
theorem List.coe_toFinsupp {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => List.getD l x 0 0] :
↑() = fun x => List.getD l x 0
@[simp]
theorem List.toFinsupp_apply {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => List.getD l x 0 0] (i : ) :
↑() i = List.getD l i 0
theorem List.toFinsupp_support {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => List.getD l x 0 0] :
().support = Finset.filter (fun x => List.getD l x 0 0) ()
theorem List.toFinsupp_apply_lt {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => List.getD l x 0 0] (n : ) (hn : n < ) :
↑() n = List.get l { val := n, isLt := hn }
theorem List.toFinsupp_apply_fin {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => List.getD l x 0 0] (n : Fin ()) :
↑() n = List.get l n
@[deprecated]
theorem List.toFinsupp_apply_lt' {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => List.getD l x 0 0] (n : ) (hn : n < ) :
↑() n = List.nthLe l n hn
theorem List.toFinsupp_apply_le {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => List.getD l x 0 0] (n : ) (hn : n) :
↑() n = 0
@[simp]
theorem List.toFinsupp_nil {M : Type u_1} [Zero M] [DecidablePred fun i => List.getD [] i 0 0] :
= 0
theorem List.toFinsupp_singleton {M : Type u_1} [Zero M] (x : M) [DecidablePred fun x => List.getD [x] x 0 0] :
= fun₀ | 0 => x
@[simp]
theorem List.toFinsupp_cons_apply_zero {M : Type u_1} [Zero M] (x : M) (xs : List M) [DecidablePred fun x => List.getD (x :: xs) x 0 0] :
↑(List.toFinsupp (x :: xs)) 0 = x
@[simp]
theorem List.toFinsupp_cons_apply_succ {M : Type u_1} [Zero M] (x : M) (xs : List M) (n : ) [DecidablePred fun x => List.getD (x :: xs) x 0 0] [DecidablePred fun x => List.getD xs x 0 0] :
↑(List.toFinsupp (x :: xs)) () = ↑() n
theorem List.toFinsupp_append {R : Type u_2} [] (l₁ : List R) (l₂ : List R) [DecidablePred fun x => List.getD (l₁ ++ l₂) x 0 0] [DecidablePred fun x => List.getD l₁ x 0 0] [DecidablePred fun x => List.getD l₂ x 0 0] :
List.toFinsupp (l₁ ++ l₂) =
theorem List.toFinsupp_cons_eq_single_add_embDomain {R : Type u_2} [] (x : R) (xs : List R) [DecidablePred fun x => List.getD (x :: xs) x 0 0] [DecidablePred fun x => List.getD xs x 0 0] :
List.toFinsupp (x :: xs) = (fun₀ | 0 => x) + Finsupp.embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } ()
theorem List.toFinsupp_concat_eq_toFinsupp_add_single {R : Type u_2} [] (x : R) (xs : List R) [DecidablePred fun i => List.getD (xs ++ [x]) i 0 0] [DecidablePred fun i => List.getD xs i 0 0] :
List.toFinsupp (xs ++ [x]) = + fun₀ | => x
theorem List.toFinsupp_eq_sum_map_enum_single {R : Type u_2} [] (l : List R) [DecidablePred fun x => List.getD l x 0 0] :
= List.sum (List.map (fun nr => fun₀ | nr.fst => nr.snd) ())