Documentation

Batteries.Data.List.Scan

List scan #

Prove basic results about List.scanl, List.scanr, List.scanlM and List.scanrM.

partialSums/partialProd #

source
@[simp]
theorem List.length_partialSums {α : Type u_1} [Add α] [Zero α] {l : List α} :
l.partialSums.length = l.length + 1
source
@[simp]
theorem List.partialSums_ne_nil {α : Type u_1} [Add α] [Zero α] {l : List α} :
l.partialSums ≠ []
source
@[simp]
theorem List.partialSums_nil {α : Type u_1} [Add α] [Zero α] :
[].partialSums = [0]
source
theorem List.partialSums_cons {α : Type u_1} {a : α} [Add α] [Zero α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] {l : List α} :
(a :: l).partialSums = 0 :: map (fun (x : α) => a + x) l.partialSums
source
theorem List.partialSums_append {α : Type u_1} [Add α] [Zero α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] {l₁ l₂ : List α} :
(l₁ ++ l₂).partialSums = l₁.partialSums ++ map (fun (x : α) => l₁.sum + x) l₂.partialSums.tail
source
@[simp]
theorem List.getElem_partialSums {α : Type u_1} {i : Nat} [Add α] [Zero α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] {l : List α} (h : i < l.partialSums.length) :
l.partialSums[i] = (take i l).sum
source
@[simp]
theorem List.getElem?_partialSums {α : Type u_1} {i : Nat} [Add α] [Zero α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] {l : List α} :
l.partialSums[i]? = if i ≤ l.length then some (take i l).sum else none
source
@[simp]
theorem List.take_partialSums {α : Type u_1} {i : Nat} [Add α] [Zero α] {l : List α} :
take (i + 1) l.partialSums = (take i l).partialSums
source
@[simp]
theorem List.length_partialProds {α : Type u_1} [Mul α] [One α] {l : List α} :
l.partialProds.length = l.length + 1
source
@[simp]
theorem List.partialProds_nil {α : Type u_1} [Mul α] [One α] :
[].partialProds = [1]
source
theorem List.partialProds_cons {α : Type u_1} {a : α} [Mul α] [One α] [Std.Associative fun (x1 x2 : α) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] {l : List α} :
(a :: l).partialProds = 1 :: map (fun (x : α) => a * x) l.partialProds
source
theorem List.partialProds_append {α : Type u_1} [Mul α] [One α] [Std.Associative fun (x1 x2 : α) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] {l₁ l₂ : List α} :
(l₁ ++ l₂).partialProds = l₁.partialProds ++ map (fun (x : α) => l₁.prod * x) l₂.partialProds.tail
source
@[simp]
theorem List.getElem_partialProds {α : Type u_1} {i : Nat} [Mul α] [One α] [Std.Associative fun (x1 x2 : α) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] {l : List α} (h : i < l.partialProds.length) :
l.partialProds[i] = (take i l).prod
source
@[simp]
theorem List.getElem?_partialProds {α : Type u_1} {i : Nat} [Mul α] [One α] [Std.Associative fun (x1 x2 : α) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] {l : List α} :
l.partialProds[i]? = if i ≤ l.length then some (take i l).prod else none
source
@[simp]
theorem List.take_partialProds {α : Type u_1} {i : Nat} [Mul α] [One α] {l : List α} :
take (i + 1) l.partialProds = (take i l).partialProds

flatten #

source
theorem List.length_flatten_mem_partialSums_map_length {α : Type u_1} (L : List (List α)) :
L.flatten.length ∈ (map length L).partialSums
source
theorem List.getElem_flatten_aux₁ {α : Type u_1} (L : List (List α)) (i : Nat) (h : i < L.flatten.length) :
findIdx (fun (x : Nat) => decide (x > i)) (map length L).partialSums - 1 < L.length
source
theorem List.getElem_flatten_aux₂ {α : Type u_1} (L : List (List α)) (i : Nat) (h : i < L.flatten.length) :
let j := findIdx (fun (x : Nat) => decide (x > i)) (map length L).partialSums - 1; have hj := ⋯; have k := i - (take j L).flatten.length; k < L[j].length
source
theorem List.getElem_flatten {α : Type u_1} (L : List (List α)) (i : Nat) (h : i < L.flatten.length) :
L.flatten[i] = let j := findIdx (fun (x : Nat) => decide (x > i)) (map length L).partialSums - 1; have hj := ⋯; let k := i - (take j L).flatten.length; have hk := ⋯; L[j][k]

Indexing into a flattened list: L.flatten[i] equals L[j][k] where j is the sublist index and k is the offset within that sublist.

The indices are computed as:

  • j is one less than where the cumulative sum first exceeds i
  • k is i minus the total length of the first j sublists

This theorem states that these indices are in range and the equality holds.