Minimum and maximum of lists

Main definitions

The main definitions are argmax, argmin, minimum and maximum for lists.

argmax f l returns some a, where a of l that maximises f a. If there are a b such that f a = f b, it returns whichever of a or b comes first in the list. argmax f [] = none

minimum l returns a WithTop α, the smallest element of l for nonempty lists, and ⊤ for []

def List.argAux {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a : Option α) (b : α) : Option α

Auxiliary definition for argmax and argmin.

Equations

• List.argAux r a b = Option.casesOn a (some b) fun (c : α) => if r b c then some b else some c

@[simp]

theorem List.foldl_argAux_eq_none {α : Type u_1} (r : α → α → Prop) [DecidableRel r] {l : List α} {o : Option α} : foldl (argAux r) o l = none ↔ l = [] ∧ o = none

@[simp]

theorem List.argAux_self {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (hr₀ : Irreflexive r) (a : α) : argAux r (some a) a = some a

theorem List.not_of_mem_foldl_argAux {α : Type u_1} (r : α → α → Prop) [DecidableRel r] {l : List α} (hr₀ : Irreflexive r) (hr₁ : Transitive r) {a m : α} {o : Option α} : a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m

def List.argmax {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] (f : α → β) (l : List α) : Option α

argmax f l returns some a, where f a is maximal among the elements of l, in the sense that there is no b ∈ l with f a < f b. If a, b are such that f a = f b, it returns whichever of a or b comes first in the list. argmax f [] = none.

Equations

• List.argmax f l = List.foldl (List.argAux fun (b c : α) => f c < f b) none l

def List.argmin {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] (f : α → β) (l : List α) : Option α

argmin f l returns some a, where f a is minimal among the elements of l, in the sense that there is no b ∈ l with f b < f a. If a, b are such that f a = f b, it returns whichever of a or b comes first in the list. argmin f [] = none.

Equations

• List.argmin f l = List.foldl (List.argAux fun (b c : α) => f b < f c) none l

@[simp]

theorem List.argmax_nil {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] (f : α → β) : argmax f [] = none

@[simp]

theorem List.argmin_nil {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] (f : α → β) : argmin f [] = none

@[simp]

theorem List.argmax_singleton {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] {f : α → β} {a : α} : argmax f [a] = some a

@[simp]

theorem List.argmin_singleton {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] {f : α → β} {a : α} : argmin f [a] = some a

theorem List.not_lt_of_mem_argmax {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] {f : α → β} {l : List α} {a m : α} : a ∈ l → m ∈ argmax f l → ¬f m < f a

theorem List.not_lt_of_mem_argmin {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] {f : α → β} {l : List α} {a m : α} : a ∈ l → m ∈ argmin f l → ¬f a < f m

theorem List.argmax_concat {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] (f : α → β) (a : α) (l : List α) : argmax f (l ++ [a]) = Option.casesOn (argmax f l) (some a) fun (c : α) => if f c < f a then some a else some c

theorem List.argmin_concat {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] (f : α → β) (a : α) (l : List α) : argmin f (l ++ [a]) = Option.casesOn (argmin f l) (some a) fun (c : α) => if f a < f c then some a else some c

theorem List.argmax_mem {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] {f : α → β} {l : List α} {m : α} : m ∈ argmax f l → m ∈ l

theorem List.argmin_mem {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] {f : α → β} {l : List α} {m : α} : m ∈ argmin f l → m ∈ l

@[simp]

theorem List.argmax_eq_none {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] {f : α → β} {l : List α} : argmax f l = none ↔ l = []

@[simp]

theorem List.argmin_eq_none {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLT β] {f : α → β} {l : List α} : argmin f l = none ↔ l = []

theorem List.le_of_mem_argmax {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : α → β} {l : List α} {a m : α} : a ∈ l → m ∈ argmax f l → f a ≤ f m

theorem List.le_of_mem_argmin {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : α → β} {l : List α} {a m : α} : a ∈ l → m ∈ argmin f l → f m ≤ f a

theorem List.argmax_cons {α : Type u_1} {β : Type u_2} [LinearOrder β] (f : α → β) (a : α) (l : List α) : argmax f (a :: l) = Option.casesOn (argmax f l) (some a) fun (c : α) => if f a < f c then some c else some a

theorem List.argmin_cons {α : Type u_1} {β : Type u_2} [LinearOrder β] (f : α → β) (a : α) (l : List α) : argmin f (a :: l) = Option.casesOn (argmin f l) (some a) fun (c : α) => if f c < f a then some c else some a

theorem List.index_of_argmax {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : α → β} [DecidableEq α] {l : List α} {m : α} : m ∈ argmax f l → ∀ {a : α}, a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l

theorem List.index_of_argmin {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : α → β} [DecidableEq α] {l : List α} {m : α} : m ∈ argmin f l → ∀ {a : α}, a ∈ l → f a ≤ f m → idxOf m l ≤ idxOf a l

theorem List.mem_argmax_iff {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : α → β} {l : List α} {m : α} [DecidableEq α] : m ∈ argmax f l ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l

theorem List.argmax_eq_some_iff {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : α → β} {l : List α} {m : α} [DecidableEq α] : argmax f l = some m ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l

theorem List.mem_argmin_iff {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : α → β} {l : List α} {m : α} [DecidableEq α] : m ∈ argmin f l ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f m ≤ f a) ∧ ∀ (a : α), a ∈ l → f a ≤ f m → idxOf m l ≤ idxOf a l

theorem List.argmin_eq_some_iff {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : α → β} {l : List α} {m : α} [DecidableEq α] : argmin f l = some m ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f m ≤ f a) ∧ ∀ (a : α), a ∈ l → f a ≤ f m → idxOf m l ≤ idxOf a l

def List.maximum {α : Type u_1} [Preorder α] [DecidableLT α] (l : List α) : WithBot α

maximum l returns a WithBot α, the largest element of l for nonempty lists, and ⊥ for []

Equations

• l.maximum = List.argmax id l

def List.minimum {α : Type u_1} [Preorder α] [DecidableLT α] (l : List α) : WithTop α

minimum l returns a WithTop α, the smallest element of l for nonempty lists, and ⊤ for []

Equations

• l.minimum = List.argmin id l

@[simp]

theorem List.maximum_nil {α : Type u_1} [Preorder α] [DecidableLT α] : [].maximum = ⊥

@[simp]

theorem List.minimum_nil {α : Type u_1} [Preorder α] [DecidableLT α] : [].minimum = ⊤

@[simp]

theorem List.maximum_singleton {α : Type u_1} [Preorder α] [DecidableLT α] (a : α) : [a].maximum = ↑a

@[simp]

theorem List.minimum_singleton {α : Type u_1} [Preorder α] [DecidableLT α] (a : α) : [a].minimum = ↑a

theorem List.maximum_mem {α : Type u_1} [Preorder α] [DecidableLT α] {l : List α} {m : α} : l.maximum = ↑m → m ∈ l

theorem List.minimum_mem {α : Type u_1} [Preorder α] [DecidableLT α] {l : List α} {m : α} : l.minimum = ↑m → m ∈ l

@[simp]

theorem List.maximum_eq_bot {α : Type u_1} [Preorder α] [DecidableLT α] {l : List α} : l.maximum = ⊥ ↔ l = []

@[simp]

theorem List.minimum_eq_top {α : Type u_1} [Preorder α] [DecidableLT α] {l : List α} : l.minimum = ⊤ ↔ l = []

theorem List.not_maximum_lt_of_mem {α : Type u_1} [Preorder α] [DecidableLT α] {l : List α} {a m : α} : a ∈ l → l.maximum = ↑m → ¬m < a

theorem List.not_lt_minimum_of_mem {α : Type u_1} [Preorder α] [DecidableLT α] {l : List α} {a m : α} : a ∈ l → l.minimum = ↑m → ¬a < m

theorem List.not_maximum_lt_of_mem' {α : Type u_1} [Preorder α] [DecidableLT α] {l : List α} {a : α} (ha : a ∈ l) : ¬l.maximum < ↑a

theorem List.not_lt_minimum_of_mem' {α : Type u_1} [Preorder α] [DecidableLT α] {l : List α} {a : α} (ha : a ∈ l) : ¬↑a < l.minimum

theorem List.maximum_concat {α : Type u_1} [LinearOrder α] (a : α) (l : List α) : (l ++ [a]).maximum = max l.maximum ↑a

theorem List.le_maximum_of_mem {α : Type u_1} [LinearOrder α] {l : List α} {a m : α} : a ∈ l → l.maximum = ↑m → a ≤ m

theorem List.minimum_le_of_mem {α : Type u_1} [LinearOrder α] {l : List α} {a m : α} : a ∈ l → l.minimum = ↑m → m ≤ a

theorem List.le_maximum_of_mem' {α : Type u_1} [LinearOrder α] {l : List α} {a : α} (ha : a ∈ l) : ↑a ≤ l.maximum

theorem List.minimum_le_of_mem' {α : Type u_1} [LinearOrder α] {l : List α} {a : α} (ha : a ∈ l) : l.minimum ≤ ↑a

theorem List.minimum_concat {α : Type u_1} [LinearOrder α] (a : α) (l : List α) : (l ++ [a]).minimum = min l.minimum ↑a

theorem List.maximum_cons {α : Type u_1} [LinearOrder α] (a : α) (l : List α) : (a :: l).maximum = max (↑a) l.maximum

theorem List.minimum_cons {α : Type u_1} [LinearOrder α] (a : α) (l : List α) : (a :: l).minimum = min (↑a) l.minimum

theorem List.maximum_append {α : Type u_1} [LinearOrder α] (l₁ l₂ : List α) : (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum

theorem List.minimum_append {α : Type u_1} [LinearOrder α] (l₁ l₂ : List α) : (l₁ ++ l₂).minimum = min l₁.minimum l₂.minimum

theorem List.maximum_le_of_forall_le {α : Type u_1} [LinearOrder α] {l : List α} {b : WithBot α} (h : ∀ (a : α), a ∈ l → ↑a ≤ b) : l.maximum ≤ b

theorem List.le_minimum_of_forall_le {α : Type u_1} [LinearOrder α] {l : List α} {b : WithTop α} (h : ∀ (a : α), a ∈ l → b ≤ ↑a) : b ≤ l.minimum

theorem List.maximum_mono {α : Type u_1} [LinearOrder α] {l₁ l₂ : List α} (h : l₁ ⊆ l₂) : l₁.maximum ≤ l₂.maximum

theorem List.minimum_anti {α : Type u_1} [LinearOrder α] {l₁ l₂ : List α} (h : l₁ ⊆ l₂) : l₂.minimum ≤ l₁.minimum

theorem List.maximum_eq_coe_iff {α : Type u_1} [LinearOrder α] {l : List α} {m : α} : l.maximum = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m

theorem List.minimum_eq_coe_iff {α : Type u_1} [LinearOrder α] {l : List α} {m : α} : l.minimum = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → m ≤ a

theorem List.coe_le_maximum_iff {α : Type u_1} [LinearOrder α] {l : List α} {a : α} : ↑a ≤ l.maximum ↔ ∃ (b : α), b ∈ l ∧ a ≤ b

theorem List.minimum_le_coe_iff {α : Type u_1} [LinearOrder α] {l : List α} {a : α} : l.minimum ≤ ↑a ↔ ∃ (b : α), b ∈ l ∧ b ≤ a

theorem List.maximum_ne_bot_of_ne_nil {α : Type u_1} [LinearOrder α] {l : List α} (h : l ≠ []) : l.maximum ≠ ⊥

theorem List.minimum_ne_top_of_ne_nil {α : Type u_1} [LinearOrder α] {l : List α} (h : l ≠ []) : l.minimum ≠ ⊤

theorem List.maximum_ne_bot_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) : l.maximum ≠ ⊥

theorem List.minimum_ne_top_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) : l.minimum ≠ ⊤

def List.maximum_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) : α

The maximum value in a non-empty List.

Equations

• List.maximum_of_length_pos h = l.maximum.unbot ⋯

def List.minimum_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) : α

The minimum value in a non-empty List.

Equations

• List.minimum_of_length_pos h = List.maximum_of_length_pos h

@[simp]

theorem List.coe_maximum_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) : ↑(maximum_of_length_pos h) = l.maximum

@[simp]

theorem List.coe_minimum_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) : ↑(minimum_of_length_pos h) = l.minimum

@[simp]

theorem List.le_maximum_of_length_pos_iff {α : Type u_1} [LinearOrder α] {l : List α} {b : α} (h : 0 < l.length) : b ≤ maximum_of_length_pos h ↔ ↑b ≤ l.maximum

@[simp]

theorem List.minimum_of_length_pos_le_iff {α : Type u_1} [LinearOrder α] {l : List α} {b : α} (h : 0 < l.length) : minimum_of_length_pos h ≤ b ↔ l.minimum ≤ ↑b

theorem List.maximum_of_length_pos_mem {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) : maximum_of_length_pos h ∈ l

theorem List.minimum_of_length_pos_mem {α : Type u_1} [LinearOrder α] {l : List α} (h : 0 < l.length) : minimum_of_length_pos h ∈ l

theorem List.le_maximum_of_length_pos_of_mem {α : Type u_1} [LinearOrder α] {l : List α} {a : α} (h : a ∈ l) (w : 0 < l.length) : a ≤ maximum_of_length_pos w

theorem List.minimum_of_length_pos_le_of_mem {α : Type u_1} [LinearOrder α] {l : List α} {a : α} (h : a ∈ l) (w : 0 < l.length) : minimum_of_length_pos w ≤ a

theorem List.getElem_le_maximum_of_length_pos {α : Type u_1} [LinearOrder α] {l : List α} {i : ℕ} (w : i < l.length) (h : 0 < l.length := ⋯) : l[i] ≤ maximum_of_length_pos h

theorem List.minimum_of_length_pos_le_getElem {α : Type u_1} [LinearOrder α] {l : List α} {i : ℕ} (w : i < l.length) (h : 0 < l.length := ⋯) : minimum_of_length_pos h ≤ l[i]

theorem List.getD_max?_eq_unbotD_maximum {α : Type u_1} [LinearOrder α] (l : List α) (d : α) : l.max?.getD d = WithBot.unbotD d l.maximum

theorem List.getD_min?_eq_untopD_minimum {α : Type u_1} [LinearOrder α] (l : List α) (d : α) : l.min?.getD d = WithTop.untopD d l.minimum

@[simp]

theorem List.foldr_max_of_ne_nil {α : Type u_1} [LinearOrder α] [OrderBot α] {l : List α} (h : l ≠ []) : ↑(foldr max ⊥ l) = l.maximum

theorem List.max_le_of_forall_le {α : Type u_1} [LinearOrder α] [OrderBot α] (l : List α) (a : α) (h : ∀ (x : α), x ∈ l → x ≤ a) : foldr max ⊥ l ≤ a

theorem List.le_max_of_le {α : Type u_1} [LinearOrder α] [OrderBot α] {l : List α} {a x : α} (hx : x ∈ l) (h : a ≤ x) : a ≤ foldr max ⊥ l

@[simp]

theorem List.foldr_min_of_ne_nil {α : Type u_1} [LinearOrder α] [OrderTop α] {l : List α} (h : l ≠ []) : ↑(foldr min ⊤ l) = l.minimum

theorem List.le_min_of_forall_le {α : Type u_1} [LinearOrder α] [OrderTop α] (l : List α) (a : α) (h : ∀ (x : α), x ∈ l → a ≤ x) : a ≤ foldr min ⊤ l

theorem List.min_le_of_le {α : Type u_1} [LinearOrder α] [OrderTop α] (l : List α) (a : α) {x : α} (hx : x ∈ l) (h : x ≤ a) : foldr min ⊤ l ≤ a

theorem List.le_max_of_le' {α : Type u_1} [LinearOrder α] {l : List α} {a x : α} (b : α) (hx : x ∈ l) (h : a ≤ x) : a ≤ foldr max b l

If a ≤ x for some x in the list l, and b : α, then a ≤ l.foldr max b.

theorem List.min_le_of_le' {α : Type u_1} [LinearOrder α] {l : List α} {a x : α} (b : α) (hx : x ∈ l) (h : x ≤ a) : foldr min b l ≤ a