Minimum and maximum of lists #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
[]
def
list.arg_aux
{α : Type u_1}
(r : α → α → Prop)
[decidable_rel r]
(a : option α)
(b : α) :
option α
Auxiliary definition for argmax and argmin.
Equations
- list.arg_aux r a b = a.cases_on (option.some b) (λ (c : α), ite (r b c) (option.some b) (option.some c))
@[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
@[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
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
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
- list.argmax f l = list.foldl (list.arg_aux (λ (b c : α), f c < f b)) option.none l
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
- list.argmin f l = list.foldl (list.arg_aux (λ (b c : α), f b < f c)) option.none l
@[simp]
theorem
list.argmax_nil
{α : Type u_1}
{β : Type u_2}
[preorder β]
[decidable_rel has_lt.lt]
(f : α → β) :
@[simp]
theorem
list.argmin_nil
{α : Type u_1}
{β : Type u_2}
[preorder β]
[decidable_rel has_lt.lt]
(f : α → β) :
@[simp]
theorem
list.argmax_singleton
{α : Type u_1}
{β : Type u_2}
[preorder β]
[decidable_rel has_lt.lt]
{f : α → β}
{a : α} :
list.argmax f [a] = ↑a
@[simp]
theorem
list.argmin_singleton
{α : Type u_1}
{β : Type u_2}
[preorder β]
[decidable_rel has_lt.lt]
{f : α → β}
{a : α} :
list.argmin f [a] = ↑a
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))
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))
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
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
@[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
@[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
theorem
list.le_of_mem_argmax
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{l : list α}
{a m : α} :
theorem
list.le_of_mem_argmin
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{l : list α}
{a m : α} :
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))
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))
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
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
theorem
list.mem_argmax_iff
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{l : list α}
{m : α}
[decidable_eq α] :
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
theorem
list.mem_argmin_iff
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{l : list α}
{m : α}
[decidable_eq α] :
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
maximum l returns an with_bot α, the largest element of l for nonempty lists, and ⊥ for
[]
Equations
- l.maximum = list.argmax id l
minimum l returns an with_top α, the smallest element of l for nonempty lists, and ⊤ for
[]
Equations
- l.minimum = list.argmin id l
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[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
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
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
@[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
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
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