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.arg_aux {α : Type u_1} (r : α → α → Prop) [decidable_rel r] (a : option α) (b : α) :
option α

Auxiliary definition for argmax and argmin.

Equations
source
@[simp]
theorem list.foldl_arg_aux_eq_none {α : Type u_1} (r : α → α → Prop) [decidable_rel r] {l : list α} {o : option α} :
list.foldl (list.arg_aux r) o l = option.none ↔ l = list.nil ∧ o = option.none
source
@[simp]
theorem list.arg_aux_self {α : Type u_1} (r : α → α → Prop) [decidable_rel r] (hr₀ : irreflexive r) (a : α) :
list.arg_aux r (option.some a) a = ↑a
source
theorem list.not_of_mem_foldl_arg_aux {α : Type u_1} (r : α → α → Prop) [decidable_rel r] {l : list α} (hr₀ : irreflexive r) (hr₁ : transitive r) {a m : α} {o : option α} :
a ∈ l → m ∈ list.foldl (list.arg_aux r) o l → ¬r a m
source
def list.argmax {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] (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
source
def list.argmin {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] (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
source
@[simp]
theorem list.argmax_nil {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] (f : α → β) :
list.argmax f list.nil = option.none
source
@[simp]
theorem list.argmin_nil {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] (f : α → β) :
list.argmin f list.nil = option.none
source
@[simp]
theorem list.argmax_singleton {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] {f : α → β} {a : α} :
list.argmax f [a] = ↑a
source
@[simp]
theorem list.argmin_singleton {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] {f : α → β} {a : α} :
list.argmin f [a] = ↑a
source
theorem list.not_lt_of_mem_argmax {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] {f : α → β} {l : list α} {a m : α} :
a ∈ l → m ∈ list.argmax f l → ¬f m < f a
source
theorem list.not_lt_of_mem_argmin {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] {f : α → β} {l : list α} {a m : α} :
a ∈ l → m ∈ list.argmin f l → ¬f a < f m
source
theorem list.argmax_concat {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] (f : α → β) (a : α) (l : list α) :
list.argmax f (l ++ [a]) = (list.argmax f l).cases_on (option.some a) (λ (c : α), ite (f c < f a) (option.some a) (option.some c))
source
theorem list.argmin_concat {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] (f : α → β) (a : α) (l : list α) :
list.argmin f (l ++ [a]) = (list.argmin f l).cases_on (option.some a) (λ (c : α), ite (f a < f c) (option.some a) (option.some c))
source
theorem list.argmax_mem {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] {f : α → β} {l : list α} {m : α} :
m ∈ list.argmax f l → m ∈ l
source
theorem list.argmin_mem {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] {f : α → β} {l : list α} {m : α} :
m ∈ list.argmin f l → m ∈ l
source
@[simp]
theorem list.argmax_eq_none {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] {f : α → β} {l : list α} :
list.argmax f l = option.none ↔ l = list.nil
source
@[simp]
theorem list.argmin_eq_none {α : Type u_1} {β : Type u_2} [preorder β] [decidable_rel has_lt.lt] {f : α → β} {l : list α} :
list.argmin f l = option.none ↔ l = list.nil
source
theorem list.le_of_mem_argmax {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {l : list α} {a m : α} :
a ∈ l → m ∈ list.argmax f l → f a ≤ f m
source
theorem list.le_of_mem_argmin {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {l : list α} {a m : α} :
a ∈ l → m ∈ list.argmin f l → f m ≤ f a
source
theorem list.argmax_cons {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) (a : α) (l : list α) :
list.argmax f (a :: l) = (list.argmax f l).cases_on (option.some a) (λ (c : α), ite (f a < f c) (option.some c) (option.some a))
source
theorem list.argmin_cons {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) (a : α) (l : list α) :
list.argmin f (a :: l) = (list.argmin f l).cases_on (option.some a) (λ (c : α), ite (f c < f a) (option.some c) (option.some a))
source
theorem list.index_of_argmax {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} [decidable_eq α] {l : list α} {m : α} :
m ∈ list.argmax f l → ∀ {a : α}, a ∈ l → f m ≤ f a → list.index_of m l ≤ list.index_of a l
source
theorem list.index_of_argmin {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} [decidable_eq α] {l : list α} {m : α} :
m ∈ list.argmin f l → ∀ {a : α}, a ∈ l → f a ≤ f m → list.index_of m l ≤ list.index_of a l
source
theorem list.mem_argmax_iff {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {l : list α} {m : α} [decidable_eq α] :
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} [linear_order β] {f : α → β} {l : list α} {m : α} [decidable_eq α] :
list.argmax f l = option.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} [linear_order β] {f : α → β} {l : list α} {m : α} [decidable_eq α] :
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} [linear_order β] {f : α → β} {l : list α} {m : α} [decidable_eq α] :
list.argmin f l = option.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} [preorder α] [decidable_rel has_lt.lt] (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} [preorder α] [decidable_rel has_lt.lt] (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} [preorder α] [decidable_rel has_lt.lt] :
list.nil.maximum = ⊥
source
@[simp]
theorem list.minimum_nil {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] :
list.nil.minimum = ⊤
source
@[simp]
theorem list.maximum_singleton {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] (a : α) :
[a].maximum = ↑a
source
@[simp]
theorem list.minimum_singleton {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] (a : α) :
[a].minimum = ↑a
source
theorem list.maximum_mem {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] {l : list α} {m : α} :
l.maximum = ↑m → m ∈ l
source
theorem list.minimum_mem {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] {l : list α} {m : α} :
l.minimum = ↑m → m ∈ l
source
@[simp]
theorem list.maximum_eq_none {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] {l : list α} :
l.maximum = option.none ↔ l = list.nil
source
@[simp]
theorem list.minimum_eq_none {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] {l : list α} :
l.minimum = option.none ↔ l = list.nil
source
theorem list.not_lt_maximum_of_mem {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] {l : list α} {a m : α} :
a ∈ l → l.maximum = ↑m → ¬m < a
source
theorem list.minimum_not_lt_of_mem {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] {l : list α} {a m : α} :
a ∈ l → l.minimum = ↑m → ¬a < m
source
theorem list.not_lt_maximum_of_mem' {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] {l : list α} {a : α} (ha : a ∈ l) :
¬l.maximum < ↑a
source
theorem list.not_lt_minimum_of_mem' {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] {l : list α} {a : α} (ha : a ∈ l) :
¬↑a < l.minimum
source
theorem list.maximum_concat {α : Type u_1} [linear_order α] (a : α) (l : list α) :
(l ++ [a]).maximum = linear_order.max l.maximum ↑a
source
theorem list.le_maximum_of_mem {α : Type u_1} [linear_order α] {l : list α} {a m : α} :
a ∈ l → l.maximum = ↑m → a ≤ m
source
theorem list.minimum_le_of_mem {α : Type u_1} [linear_order α] {l : list α} {a m : α} :
a ∈ l → l.minimum = ↑m → m ≤ a
source
theorem list.le_maximum_of_mem' {α : Type u_1} [linear_order α] {l : list α} {a : α} (ha : a ∈ l) :
↑a ≤ l.maximum
source
theorem list.le_minimum_of_mem' {α : Type u_1} [linear_order α] {l : list α} {a : α} (ha : a ∈ l) :
l.minimum ≤ ↑a
source
theorem list.minimum_concat {α : Type u_1} [linear_order α] (a : α) (l : list α) :
(l ++ [a]).minimum = linear_order.min l.minimum ↑a
source
theorem list.maximum_cons {α : Type u_1} [linear_order α] (a : α) (l : list α) :
(a :: l).maximum = linear_order.max ↑a l.maximum
source
theorem list.minimum_cons {α : Type u_1} [linear_order α] (a : α) (l : list α) :
(a :: l).minimum = linear_order.min ↑a l.minimum
source
theorem list.maximum_eq_coe_iff {α : Type u_1} [linear_order α] {l : list α} {m : α} :
l.maximum = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
source
theorem list.minimum_eq_coe_iff {α : Type u_1} [linear_order α] {l : list α} {m : α} :
l.minimum = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → m ≤ a
source
@[simp]
theorem list.foldr_max_of_ne_nil {α : Type u_1} [linear_order α] [order_bot α] {l : list α} (h : l ≠ list.nil) :
↑(list.foldr linear_order.max ⊥ l) = l.maximum
source
theorem list.max_le_of_forall_le {α : Type u_1} [linear_order α] [order_bot α] (l : list α) (a : α) (h : ∀ (x : α), x ∈ l → x ≤ a) :
list.foldr linear_order.max ⊥ l ≤ a
source
theorem list.le_max_of_le {α : Type u_1} [linear_order α] [order_bot α] {l : list α} {a x : α} (hx : x ∈ l) (h : a ≤ x) :
a ≤ list.foldr linear_order.max ⊥ l
source
@[simp]
theorem list.foldr_min_of_ne_nil {α : Type u_1} [linear_order α] [order_top α] {l : list α} (h : l ≠ list.nil) :
↑(list.foldr linear_order.min ⊤ l) = l.minimum
source
theorem list.le_min_of_forall_le {α : Type u_1} [linear_order α] [order_top α] (l : list α) (a : α) (h : ∀ (x : α), x ∈ l → a ≤ x) :
a ≤ list.foldr linear_order.min ⊤ l
source
theorem list.min_le_of_le {α : Type u_1} [linear_order α] [order_top α] (l : list α) (a : α) {x : α} (hx : x ∈ l) (h : x ≤ a) :
list.foldr linear_order.min ⊤ l ≤ a