Documentation

Mathlib.Data.List.ToFinsupp

Lists as finsupp #

Main definitions #

Main theorems #

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] :

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
Instances For
    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 = Finset.filter (fun (x : ) => l.getD x 0 0) (Finset.range l.length)
    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
    @[deprecated]
    theorem List.toFinsupp_cons_apply_zero {M : Type u_1} [Zero M] (x : M) (xs : List M) [DecidablePred fun (x_1 : ) => (x :: xs).getD x_1 0 0] :
    (x :: xs).toFinsupp 0 = x
    @[deprecated]
    theorem List.toFinsupp_cons_apply_succ {M : Type u_1} [Zero M] (x : M) (xs : List M) (n : ) [DecidablePred fun (x_1 : ) => (x :: xs).getD x_1 0 0] [DecidablePred fun (x : ) => xs.getD x 0 0] :
    (x :: xs).toFinsupp n.succ = xs.toFinsupp n
    theorem List.toFinsupp_append {R : Type u_2} [AddZeroClass R] (l₁ : List R) (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_map_enum_single {R : Type u_2} [AddMonoid R] (l : List R) [DecidablePred fun (x : ) => l.getD x 0 0] :
    l.toFinsupp = (List.map (fun (nr : × R) => Finsupp.single nr.1 nr.2) l.enum).sum