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 : ℕ) => l.getD 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

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

theorem List.coe_toFinsupp {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun (x : ℕ) => l.getD x 0 ≠ 0] : ⇑l.toFinsupp = fun (x : ℕ) => l.getD x 0

@[simp]

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

theorem List.toFinsupp_support {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun (x : ℕ) => l.getD x 0 ≠ 0] : l.toFinsupp.support = {i ∈ Finset.range l.length | l.getD i 0 ≠ 0}

theorem List.toFinsupp_apply_lt {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun (x : ℕ) => l.getD x 0 ≠ 0] (n : ℕ) (hn : n < l.length) : l.toFinsupp n = l[n]

theorem List.toFinsupp_apply_fin {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun (x : ℕ) => l.getD x 0 ≠ 0] (n : Fin l.length) : l.toFinsupp ↑n = l[n]

theorem List.toFinsupp_apply_le {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun (x : ℕ) => l.getD x 0 ≠ 0] (n : ℕ) (hn : l.length ≤ n) : l.toFinsupp n = 0

@[simp]

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

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

theorem List.toFinsupp_append {R : Type u_2} [AddZeroClass R] (l₁ l₂ : List R) [DecidablePred fun (x : ℕ) => (l₁ ++ l₂).getD x 0 ≠ 0] [DecidablePred fun (x : ℕ) => l₁.getD x 0 ≠ 0] [DecidablePred fun (x : ℕ) => l₂.getD x 0 ≠ 0] : (l₁ ++ l₂).toFinsupp = l₁.toFinsupp + Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp

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

theorem List.toFinsupp_concat_eq_toFinsupp_add_single {R : Type u_2} [AddZeroClass R] (x : R) (xs : List R) [DecidablePred fun (i : ℕ) => (xs ++ [x]).getD i 0 ≠ 0] [DecidablePred fun (i : ℕ) => xs.getD i 0 ≠ 0] : (xs ++ [x]).toFinsupp = xs.toFinsupp + Finsupp.single xs.length x

theorem List.toFinsupp_eq_sum_mapIdx_single {R : Type u_2} [AddMonoid R] (l : List R) [DecidablePred fun (x : ℕ) => l.getD x 0 ≠ 0] : l.toFinsupp = (mapIdx (fun (n : ℕ) (r : R) => Finsupp.single n r) l).sum