def List.Notation.«term_[.._]» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def List.Notation.«term_[_..]» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def List.Notation.«term..=_» : Lean.ParserDescr

Equations

• List.Notation.«term..=_» = Lean.ParserDescr.node `List.Notation.«term..=_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "..=") (Lean.ParserDescr.cat `term 0))

def List.Notation.«term‖_‖» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def List.rep {α : Type u_1} (l : List α) : ℕ → List α

Equations

• l.rep 0 = []
• l.rep n.succ = l ++ l.rep n

@[simp]

theorem List.repeat_zero {α : Type u_1} (l : List α) : l.rep 0 = []

@[simp]

theorem List.repeat_one {α : Type u_1} (l : List α) : l.rep 1 = l

@[simp]

theorem List.repeat_succ {α : Type u_1} (l : List α) {n : ℕ} : l.rep (n + 1) = l ++ l.rep n

@[simp]

theorem List.take_length_succ {α : Type} (A : List α) : A[..‖A‖ + 1] = A

Products

@[simp]

theorem List.product_length {α : Type u_1} {β : Type u_2} {as : List α} {bs : List β} : ‖as.product bs‖ = ‖as‖ * ‖bs‖

def List.products {α : Type u_1} : List (List α) → List (List α)

Equations

• [].products = [[]]
• (x_1 :: xs).products = List.map (fun (x : α × List α) => match x with | (a, as) => a :: as) (x_1.product xs.products)

@[simp]

theorem List.products_nil {α : Type u_1} : [].products = [[]]

@[simp]

theorem List.products_length {α : Type u_1} {xs : List (List α)} : ‖xs.products‖ = (map length xs).prod

@[simp]

theorem List.mem_products_length {α : Type u_1} {xs : List (List α)} {x : List α} (h : x ∈ xs.products) : ‖x‖ = ‖xs‖

@[simp]

theorem List.products_eq_nil {α : Type u_1} {xs : List (List α)} : xs.products = [] ↔ [] ∈ xs

theorem List.mem_products {α : Type u_1} {xs : List (List α)} {x : List α} : x ∈ xs.products ↔ ‖x‖ = ‖xs‖ ∧ ∀ (i : ℕ) (h : i < ‖x‖) (h' : i < ‖xs‖), x[i] ∈ xs[i]

theorem List.singleton_product {α : Type u_1} {β : Type u_3} {l : List β} {a : α} : [a].product l = map (fun (x : β) => (a, x)) l

theorem List.product_singleton {α : Type u_1} {β : Type u_3} {l : List β} {a : α} : l.product [a] = map (fun (x : β) => (x, a)) l

theorem List.products_append {α : Type u_1} {xs ys : List (List α)} : (xs ++ ys).products = map (fun (x : List α × List α) => match x with | (x, y) => x ++ y) (xs.products.product ys.products)

Partitions

def List.partitions {α : Type u_1} [DecidableEq α] (xs : List α) : Finset (List (List α))

Equations

• [].partitions = {[]}
• (x :: xs_2).partitions = xs_2.partitions.biUnion fun (ys : List (List α)) => match ys with | [] => {[[x]]} | y :: ys => {(x :: y) :: ys, [x] :: y :: ys}

@[simp]

theorem List.partitions_nil {α : Type u_1} [DecidableEq α] : [].partitions = {[]}

theorem List.mem_partitions_iff {α : Type u_1} [DecidableEq α] {xs : List α} {ys : List (List α)} : ys ∈ xs.partitions ↔ ys.flatten = xs ∧ ∀ y ∈ ys, y ≠ []

@[simp]

theorem List.nil_mem_partitions {α : Type u_1} [DecidableEq α] {xs : List α} : [] ∈ xs.partitions ↔ xs = []

theorem List.partitions_cons_eq_split {α : Type u_2} {𝒮 : Type u_3} [NonUnitalSemiring 𝒮] [DecidableEq α] {x : α} {xs : List α} {f : List (List α) → 𝒮} : ∑ ys ∈ (x :: xs).partitions, f ys = ∑ i ∈ ..=‖xs‖, ∑ p ∈ xs[i..].partitions, f ((x :: xs[..i]) :: p)

theorem List.mem_products' {α : Type u_2} {x : List α} {xs : List (List α)} [Inhabited α] : x ∈ xs.products ↔ ‖x‖ = ‖xs‖ ∧ ∀ i < ‖xs‖, x[i]! ∈ xs[i]!

def List.partitions' {α : Type u_1} [DecidableEq α] (xs : List α) (n : ℕ) : Finset (List (ℕ × List α))

Equations

• One or more equations did not get rendered due to their size.
• [].partitions' n = {[]}

@[simp]

theorem List.partitions'_nil {α : Type u_1} [DecidableEq α] {n : ℕ} : [].partitions' n = {[]}

theorem List.partitions_eq_partitions' {α : Type u_1} [DecidableEq α] {xs : List α} {n : ℕ} : xs.partitions = Finset.image (fun (l : List (ℕ × List α)) => map Prod.snd l) (xs.partitions' n)

theorem List.mem_partitions'_iff {α : Type u_1} [DecidableEq α] {xs : List α} {n : ℕ} {ys : List (ℕ × List α)} : ys ∈ xs.partitions' n ↔ (map Prod.snd ys).flatten = xs ∧ ∀ (a : ℕ) (b : List α), (a, b) ∈ ys → a ≤ n ∧ ¬b = []

def List.partitionsFill' {α : Type u_1} [DecidableEq α] (xs : List α) (n : ℕ) : Finset (List (List α))

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def List.buckets {α : Type u_1} [DecidableEq α] (xs : List α) (n : ℕ) : Finset (List (List α))

Equations

• One or more equations did not get rendered due to their size.
• xs.buckets 0 = ∅
• [].buckets n_1.succ = {List.replicate (n_1 + 1) []}

@[simp]

theorem List.buckets_nil {α : Type u_1} [DecidableEq α] {n : ℕ} : [].buckets n = if n = 0 then ∅ else {replicate n []}

@[simp]

theorem List.buckets_zero {α : Type u_1} [DecidableEq α] (xs : List α) : xs.buckets 0 = ∅

@[simp]

theorem List.buckets_one {α : Type u_1} [DecidableEq α] (xs : List α) : xs.buckets 1 = {[xs]}

theorem List.mem_buckets_iff {α : Type u_1} [DecidableEq α] (xs : List α) (n : ℕ) {ys : List (List α)} : ys ∈ xs.buckets n ↔ n ≠ 0 ∧ ys.flatten = xs ∧ ‖ys‖ = n

theorem List.sum_le {α : Type u_2} (xs : List α) (f : α → ℕ) (cap : ℕ) (h : ∀ x ∈ xs, f x ≤ cap) : (map f xs).sum ≤ cap * ‖xs‖

theorem List.le_sum {α : Type u_2} (xs : List α) (f : α → ℕ) (cap : ℕ) (h : ∀ x ∈ xs, cap ≤ f x) : ‖xs‖ * cap ≤ (map f xs).sum

def List.count' (n m : ℕ) : ℕ

Equations

• List.count' n m = (n + 1) * (m + 1)

theorem List.count'_le {n n' m m' : ℕ} (hn : n ≤ n') (hm : m ≤ m') : count' n m ≤ count' n' m'

theorem List.partitionsFill'_subset_buckets {α : Type u_1} [DecidableEq α] (xs : List α) (n : ℕ) (h : xs ≠ []) : xs.partitionsFill' n ⊆ (Finset.range (count' ‖xs‖ n)).biUnion xs.buckets

def List.corep {α : Type u_2} (xs : List (List α)) : List (ℕ × List α)

Equations

• [].corep = []
• ([] :: xs_2).corep = match xs_2.corep with | [] => [] | (n, y) :: ys => (n + 1, y) :: ys
• (x :: xs_2).corep = (0, x) :: xs_2.corep

@[simp]

theorem List.corep_nil {α : Type u_2} : [].corep = []

@[simp]

theorem List.corep_mem_ne_nil {α : Type u_2} {ls : List (List α)} {x : ℕ × List α} (h : x ∈ ls.corep) : ls ≠ []

@[simp]

theorem List.corep_mem_ne_nil' {α : Type u_2} {ls : List (List α)} {x : ℕ × List α} (h : x ∈ ls.corep) : x.2 ≠ []

@[simp]

theorem List.corep_mem_lt {α : Type u_2} {ls : List (List α)} {x : ℕ × List α} (h : x ∈ ls.corep) : x.1 < ‖ls‖

@[simp]

theorem List.corep_flatten {α : Type u_2} {ls : List (List α)} : (map Prod.snd ls.corep).flatten = ls.flatten

@[simp]

theorem List.corep_replicate_nil {α : Type u_2} {i : ℕ} : (replicate i []).corep = []

@[simp]

theorem List.corep_append_replicate_nil {α : Type u_2} {ls : List (List α)} {i : ℕ} : (ls ++ replicate i []).corep = ls.corep

theorem List.corep_reconstruct {α : Type u_2} {ls : List (List α)} : flatMap (fun (x : ℕ × List α) => replicate x.1 [] ++ [x.2]) ls.corep ++ rtakeWhile (fun (x : List α) => decide (‖x‖ = 0)) ls = ls

theorem List.exists_nil_tail {α : Type u_2} (xs : List (List α)) : ∃ (ys : List (List α)), (∃ (x : ℕ), ys ++ replicate x [] = xs) ∧ ∀ (h : ¬ys = []), ¬ys.getLast h = []

theorem List.buckets_subset_partitionsFill' {α : Type u_1} [DecidableEq α] (xs : List α) (n : ℕ) (h : xs ≠ []) : (Finset.range n).biUnion xs.buckets ⊆ xs.partitionsFill' (count' ‖xs‖ n)

theorem List.sum_partitions'_cons {𝒮' : Type u_2} [NonUnitalSemiring 𝒮'] {ι : Type u_3} [DecidableEq ι] {x : ι} {xs : List ι} {n : ℕ} {f : List (ℕ × List ι) → 𝒮'} : ∑ ys ∈ (x :: xs).partitions' n, f ys = if xs = [] then ∑ i ∈ ..=n, f [(i, [x])] else ∑ ys ∈ xs.partitions' n, (f ((ys.head!.1, x :: ys.head!.2) :: ys.tail) + ∑ i ∈ Finset.image (fun (j : ℕ) => (j, [x]) :: ys) (..=n), f i)

theorem List.sum_partitionsFill' {𝒮' : Type u_2} [NonUnitalSemiring 𝒮'] {ι : Type u_3} [DecidableEq ι] {xs : List ι} {n : ℕ} {f : List (List ι) → 𝒮'} : ∑ ys ∈ xs.partitionsFill' n, f ys = ∑ x ∈ xs.partitions' n, ∑ x_1 ∈ ..=n, f (flatMap (fun (x : ℕ × List ι) => replicate x.1 [] ++ [x.2]) x ++ replicate x_1 [])

theorem List.sum_partitionsFill'_cons {𝒮' : Type u_2} [NonUnitalSemiring 𝒮'] {ι : Type u_3} [DecidableEq ι] {x : ι} {xs : List ι} {n : ℕ} {f : List (List ι) → 𝒮'} (h : xs ≠ []) (hf : ∀ (a b : List (List ι)), f (a ++ b) = f a * f b) : ∑ ys ∈ (x :: xs).partitionsFill' n, f ys = (∑ i ∈ xs.partitions' n, f (replicate i.head!.1 []) * f [x :: i.head!.2] * f (flatMap (fun (x : ℕ × List ι) => replicate x.1 [] ++ [x.2]) i.tail)) * ∑ i ∈ ..=n, f (replicate i []) + ∑ i ∈ ..=n, ∑ ys ∈ xs.partitionsFill' n, f (replicate i [] ++ [x] :: ys)

theorem List.mul_prod_mul_eq {α : Type u_2} {ι : Type u_3} [Semiring α] {xs : List ι} {a : α} {f : ι → α} : a * (map (fun (x : ι) => f x * a) xs).prod = (map (fun (x : ι) => a * f x) xs).prod * a

@[simp]

theorem List.buckets_pairwise_disjoint {α : Type u_2} [DecidableEq α] {xs : List α} {S : Set ℕ} : S.PairwiseDisjoint xs.buckets

@[simp]

theorem List.buckets_succ_pairwise_disjoint {α : Type u_2} [DecidableEq α] {xs : List α} {S : Set ℕ} : S.PairwiseDisjoint fun (x : ℕ) => xs.buckets x.succ