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
[]
def
list.argmax₂
{α : Type u_1}
{β : Type u_2}
[linear_order β]
(f : α → β)
(a : option α)
(b : α) :
option α
Auxiliary definition to define argmax
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
- list.argmax f l = list.foldl (list.argmax₂ f) none l
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
- list.argmin f l = list.argmax f l
@[simp]
theorem
list.argmax_two_self
{α : Type u_1}
{β : Type u_2}
[linear_order β]
(f : α → β)
(a : α) :
list.argmax₂ f (some a) a = ↑a
@[simp]
@[simp]
@[simp]
theorem
list.argmax_singleton
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{a : α} :
list.argmax f [a] = some a
@[simp]
theorem
list.argmin_singleton
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{a : α} :
list.argmin f [a] = ↑a
@[simp]
theorem
list.foldl_argmax₂_eq_none
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{l : list α}
{o : option α} :
list.foldl (list.argmax₂ f) o l = none ↔ l = list.nil ∧ o = none
theorem
list.argmax_mem
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{l : list α}
{m : α} :
m ∈ list.argmax f l → m ∈ l
theorem
list.argmin_mem
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{l : list α}
{m : α} :
m ∈ list.argmin f l → m ∈ l
@[simp]
theorem
list.argmax_eq_none
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{l : list α} :
@[simp]
theorem
list.argmin_eq_none
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{l : list α} :
theorem
list.le_argmax_of_mem
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{a m : α}
{l : list α} :
a ∈ l → m ∈ list.argmax f l → f a ≤ f m
theorem
list.argmin_le_of_mem
{α : Type u_1}
{β : Type u_2}
[linear_order β]
{f : α → β}
{a m : α}
{l : list α} :
a ∈ l → m ∈ list.argmin f l → f m ≤ f a
theorem
list.argmax_concat
{α : Type u_1}
{β : Type u_2}
[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))
theorem
list.argmin_concat
{α : Type u_1}
{β : Type u_2}
[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))
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 (some a) (λ (c : α), ite (f c ≤ f a) (some a) (some c))
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 (some a) (λ (c : α), ite (f a ≤ f c) (some a) (some c))
theorem
list.index_of_argmax
{α : Type u_1}
{β : Type u_2}
[linear_order β]
[decidable_eq α]
{f : α → β}
{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 β]
[decidable_eq α]
{f : α → β}
{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 β]
[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
theorem
list.argmax_eq_some_iff
{α : Type u_1}
{β : Type u_2}
[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
theorem
list.mem_argmin_iff
{α : Type u_1}
{β : Type u_2}
[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
theorem
list.argmin_eq_some_iff
{α : Type u_1}
{β : Type u_2}
[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
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]
Note: since there is no typeclass typeclass dual
to canonically_linear_ordered_add_monoid α we cannot express these lemmas generally for
minimum; instead we are limited to doing so on order_dual α.
theorem
list.maximum_eq_coe_foldr_max_of_ne_nil
{M : Type u_3}
[canonically_linear_ordered_add_monoid M]
(l : list M)
(h : l ≠ list.nil) :
theorem
list.minimum_eq_coe_foldr_min_of_ne_nil
{M : Type u_3}
[canonically_linear_ordered_add_monoid M]
(l : list (order_dual M))
(h : l ≠ list.nil) :
theorem
list.max_le_of_forall_le
{M : Type u_3}
[canonically_linear_ordered_add_monoid M]
(l : list M)
(n : M)
(h : ∀ (x : M), x ∈ l → x ≤ n) :
list.foldr max ⊥ l ≤ n
theorem
list.le_min_of_le_forall
{M : Type u_3}
[canonically_linear_ordered_add_monoid M]
(l : list (order_dual M))
(n : order_dual M)
(h : ∀ (x : order_dual M), x ∈ l → n ≤ x) :
n ≤ list.foldr min ⊤ l