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) or0outside of the list.
Main theorems #
List.toFinsupp_eq_sum_map_enum_single: Al : List MoverManAddMonoid, when interpreted as a finitely supported function, is equal to the sum ofFinsupp.singleproduced by mapping overList.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]
:
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 := Finset.filter (fun (i : ℕ) => l.getD i 0 ≠ 0) (Finset.range l.length), toFun := fun (i : ℕ) => l.getD i 0, mem_support_toFun := ⋯ }
Instances For
theorem
List.coe_toFinsupp
{M : Type u_1}
[Zero M]
(l : List M)
[DecidablePred fun (x : ℕ) => l.getD x 0 ≠ 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_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]
@[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_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]
:
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_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