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] : ℕ →₀ 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.onFinset construction.

Equations

• List.toFinsupp l = { support := Finset.filter (fun (i : ℕ) => List.getD l i 0 ≠ 0) (Finset.range (List.length l)), toFun := fun (i : ℕ) => List.getD l i 0, mem_support_toFun := ⋯ }

theorem List.coe_toFinsupp {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun (x : ℕ) => List.getD l x 0 ≠ 0] : ⇑(List.toFinsupp l) = 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 : ℕ) : (List.toFinsupp l) 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] : (List.toFinsupp l).support = Finset.filter (fun (x : ℕ) => List.getD l x 0 ≠ 0) (Finset.range (List.length l))

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 < List.length l) : (List.toFinsupp l) 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 (List.length l)) : (List.toFinsupp l) ↑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 < List.length l) : (List.toFinsupp l) 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 : List.length l ≤ n) : (List.toFinsupp l) n = 0

@[simp]

theorem List.toFinsupp_nil {M : Type u_1} [Zero M] [DecidablePred fun (i : ℕ) => List.getD [] i 0 ≠ 0] : List.toFinsupp [] = 0

theorem List.toFinsupp_singleton {M : Type u_1} [Zero M] (x : M) [DecidablePred fun (x_1 : ℕ) => List.getD [x] x_1 0 ≠ 0] : List.toFinsupp [x] = Finsupp.single 0 x

@[simp]

theorem List.toFinsupp_cons_apply_zero {M : Type u_1} [Zero M] (x : M) (xs : List M) [DecidablePred fun (x_1 : ℕ) => List.getD (x :: xs) x_1 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_1 : ℕ) => List.getD (x :: xs) x_1 0 ≠ 0] [DecidablePred fun (x : ℕ) => List.getD xs x 0 ≠ 0] : (List.toFinsupp (x :: xs)) (Nat.succ n) = (List.toFinsupp xs) n

theorem List.toFinsupp_append {R : Type u_2} [AddZeroClass R] (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₂) = List.toFinsupp l₁ + Finsupp.embDomain (addLeftEmbedding (List.length l₁)) (List.toFinsupp l₂)

theorem List.toFinsupp_cons_eq_single_add_embDomain {R : Type u_2} [AddZeroClass R] (x : R) (xs : List R) [DecidablePred fun (x_1 : ℕ) => List.getD (x :: xs) x_1 0 ≠ 0] [DecidablePred fun (x : ℕ) => List.getD xs x 0 ≠ 0] : List.toFinsupp (x :: xs) = Finsupp.single 0 x + Finsupp.embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } (List.toFinsupp xs)

theorem List.toFinsupp_concat_eq_toFinsupp_add_single {R : Type u_2} [AddZeroClass R] (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]) = List.toFinsupp xs + Finsupp.single (List.length xs) x

theorem List.toFinsupp_eq_sum_map_enum_single {R : Type u_2} [AddMonoid R] (l : List R) [DecidablePred fun (x : ℕ) => List.getD l x 0 ≠ 0] : List.toFinsupp l = List.sum (List.map (fun (nr : ℕ × R) => Finsupp.single nr.1 nr.2) (List.enum l))