mathlib documentation

data.list.min_max

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 an with_top α, the smallest element of l for nonempty lists, and ⊤ for []

source
def list.argmax₂ {α : Type u_1} {β : Type u_2} [decidable_linear_order β] (f : α → β) (a : option α) (b : α) :
option α

Auxiliary definition to define argmax

Equations
source
def list.argmax {α : Type u_1} {β : Type u_2} [decidable_linear_order β] (f : α → β) (l : list α) :
option α

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`

Equations
source
def list.argmin {α : Type u_1} {β : Type u_2} [decidable_linear_order β] (f : α → β) (l : list α) :
option α

argmin f l returns some a, where a of l that minimises 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. argmin f [] = none`

Equations
source
@[simp]
theorem list.argmax_two_self {α : Type u_1} {β : Type u_2} [decidable_linear_order β] (f : α → β) (a : α) :
list.argmax₂ f (some a) a = ↑a

source
@[simp]
theorem list.argmax_nil {α : Type u_1} {β : Type u_2} [decidable_linear_order β] (f : α → β) :
list.argmax f list.nil = none

source
@[simp]
theorem list.argmin_nil {α : Type u_1} {β : Type u_2} [decidable_linear_order β] (f : α → β) :
list.argmin f list.nil = none

source
@[simp]
theorem list.argmax_singleton {α : Type u_1} {β : Type u_2} [decidable_linear_order β] {f : α → β} {a : α} :
list.argmax f [a] = some a

source
@[simp]
theorem list.argmin_singleton {α : Type u_1} {β : Type u_2} [decidable_linear_order β] {f : α → β} {a : α} :
list.argmin f [a] = ↑a

source
@[simp]
theorem list.foldl_argmax₂_eq_none {α : Type u_1} {β : Type u_2} [decidable_linear_order β] {f : α → β} {l : list α} {o : option α} :
list.foldl (list.argmax₂ f) o l = none ↔ l = list.nil ∧ o = none

source
theorem list.argmax_mem {α : Type u_1} {β : Type u_2} [decidable_linear_order β] {f : α → β} {l : list α} {m : α} (a : m ∈ list.argmax f l) :
m ∈ l

source
theorem list.argmin_mem {α : Type u_1} {β : Type u_2} [decidable_linear_order β] {f : α → β} {l : list α} {m : α} (a : m ∈ list.argmin f l) :
m ∈ l

source
@[simp]
theorem list.argmax_eq_none {α : Type u_1} {β : Type u_2} [decidable_linear_order β] {f : α → β} {l : list α} :
list.argmax f l = none ↔ l = list.nil

source
@[simp]
theorem list.argmin_eq_none {α : Type u_1} {β : Type u_2} [decidable_linear_order β] {f : α → β} {l : list α} :
list.argmin f l = none ↔ l = list.nil

source
theorem list.le_argmax_of_mem {α : Type u_1} {β : Type u_2} [decidable_linear_order β] {f : α → β} {a m : α} {l : list α} (a_1 : a ∈ l) (a_2 : m ∈ list.argmax f l) :
f a ≤ f m

source
theorem list.argmin_le_of_mem {α : Type u_1} {β : Type u_2} [decidable_linear_order β] {f : α → β} {a m : α} {l : list α} (a_1 : a ∈ l) (a_2 : m ∈ list.argmin f l) :
f m ≤ f a

source
theorem list.argmax_concat {α : Type u_1} {β : Type u_2} [decidable_linear_order β] (f : α → β) (a : α) (l : list α) :
list.argmax f (l ++ [a]) = (list.argmax f l).cases_on (some a) (λ (c : α), ite (f a ≤ f c) (some c) (some a))

source
theorem list.argmin_concat {α : Type u_1} {β : Type u_2} [decidable_linear_order β] (f : α → β) (a : α) (l : list α) :
list.argmin f (l ++ [a]) = (list.argmin f l).cases_on (some a) (λ (c : α), ite (f c ≤ f a) (some c) (some a))

source
theorem list.argmax_cons {α : Type u_1} {β : Type u_2} [decidable_linear_order β] (f : α → β) (a : α) (l : list α) :
list.argmax f (a :: l) = (list.argmax f l).cases_on (some a) (λ (c : α), ite (f c ≤ f a) (some a) (some c))

source
theorem list.argmin_cons {α : Type u_1} {β : Type u_2} [decidable_linear_order β] (f : α → β) (a : α) (l : list α) :
list.argmin f (a :: l) = (list.argmin f l).cases_on (some a) (λ (c : α), ite (f a ≤ f c) (some a) (some c))

source
theorem list.index_of_argmax {α : Type u_1} {β : Type u_2} [decidable_linear_order β] [decidable_eq α] {f : α → β} {l : list α} {m : α} (a : m ∈ list.argmax f l) {a_1 : α} (a_2 : a_1 ∈ l) (a_3 : f m ≤ f a_1) :
list.index_of m l ≤ list.index_of a_1 l

source
theorem list.index_of_argmin {α : Type u_1} {β : Type u_2} [decidable_linear_order β] [decidable_eq α] {f : α → β} {l : list α} {m : α} (a : m ∈ list.argmin f l) {a_1 : α} (a_2 : a_1 ∈ l) (a_3 : f a_1 ≤ f m) :
list.index_of m l ≤ list.index_of a_1 l

source
theorem list.mem_argmax_iff {α : Type u_1} {β : Type u_2} [decidable_linear_order β] [decidable_eq α] {f : α → β} {m : α} {l : list α} :
m ∈ list.argmax f l ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → list.index_of m l ≤ list.index_of a l

source
theorem list.argmax_eq_some_iff {α : Type u_1} {β : Type u_2} [decidable_linear_order β] [decidable_eq α] {f : α → β} {m : α} {l : list α} :
list.argmax f l = some m ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → list.index_of m l ≤ list.index_of a l

source
theorem list.mem_argmin_iff {α : Type u_1} {β : Type u_2} [decidable_linear_order β] [decidable_eq α] {f : α → β} {m : α} {l : list α} :
m ∈ list.argmin f l ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f m ≤ f a) ∧ ∀ (a : α), a ∈ l → f a ≤ f m → list.index_of m l ≤ list.index_of a l

source
theorem list.argmin_eq_some_iff {α : Type u_1} {β : Type u_2} [decidable_linear_order β] [decidable_eq α] {f : α → β} {m : α} {l : list α} :
list.argmin f l = some m ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f m ≤ f a) ∧ ∀ (a : α), a ∈ l → f a ≤ f m → list.index_of m l ≤ list.index_of a l

source
def list.maximum {α : Type u_1} [decidable_linear_order α] (l : list α) :
with_bot α

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

Equations
source
def list.minimum {α : Type u_1} [decidable_linear_order α] (l : list α) :
with_top α

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

Equations
source
@[simp]
theorem list.maximum_nil {α : Type u_1} [decidable_linear_order α] :
list.nil.maximum = ⊥

source
@[simp]
theorem list.minimum_nil {α : Type u_1} [decidable_linear_order α] :
list.nil.minimum = ⊤

source
@[simp]
theorem list.maximum_singleton {α : Type u_1} [decidable_linear_order α] (a : α) :
[a].maximum = ↑a

source
@[simp]
theorem list.minimum_singleton {α : Type u_1} [decidable_linear_order α] (a : α) :
[a].minimum = ↑a

source
theorem list.maximum_mem {α : Type u_1} [decidable_linear_order α] {l : list α} {m : α} (a : l.maximum = ↑m) :
m ∈ l

source
theorem list.minimum_mem {α : Type u_1} [decidable_linear_order α] {l : list α} {m : α} (a : l.minimum = ↑m) :
m ∈ l

source
@[simp]
theorem list.maximum_eq_none {α : Type u_1} [decidable_linear_order α] {l : list α} :
l.maximum = none ↔ l = list.nil

source
@[simp]
theorem list.minimum_eq_none {α : Type u_1} [decidable_linear_order α] {l : list α} :
l.minimum = none ↔ l = list.nil

source
theorem list.le_maximum_of_mem {α : Type u_1} [decidable_linear_order α] {a m : α} {l : list α} (a_1 : a ∈ l) (a_2 : l.maximum = ↑m) :
a ≤ m

source
theorem list.minimum_le_of_mem {α : Type u_1} [decidable_linear_order α] {a m : α} {l : list α} (a_1 : a ∈ l) (a_2 : l.minimum = ↑m) :
m ≤ a

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

source
theorem list.le_minimum_of_mem' {α : Type u_1} [decidable_linear_order α] {a : α} {l : list α} (ha : a ∈ l) :
l.minimum ≤ ↑a

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

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

source
theorem list.maximum_cons {α : Type u_1} [decidable_linear_order α] (a : α) (l : list α) :
(a :: l).maximum = max ↑a l.maximum

source
theorem list.minimum_cons {α : Type u_1} [decidable_linear_order α] (a : α) (l : list α) :
(a :: l).minimum = min ↑a l.minimum

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

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