Auxiliary definition to define argmax
Equations
- list.argmax₂ f a b = a.cases_on (option.some b) (λ (c : α), ite (f b ≤ f c) (option.some c) (option.some b))
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) option.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}
[decidable_linear_order β]
(f : α → β)
(a : α) :
list.argmax₂ f (option.some a) a = ↑a
@[simp]
@[simp]
@[simp]
theorem
list.argmax_singleton
{α : Type u_1}
{β : Type u_2}
[decidable_linear_order β]
{f : α → β}
{a : α} :
list.argmax f [a] = option.some a
@[simp]
theorem
list.argmin_singleton
{α : Type u_1}
{β : Type u_2}
[decidable_linear_order β]
{f : α → β}
{a : α} :
list.argmin f [a] = ↑a
@[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 = option.none ↔ l = list.nil ∧ o = option.none
theorem
list.argmax_mem
{α : Type u_1}
{β : Type u_2}
[decidable_linear_order β]
{f : α → β}
{l : list α}
{m : α} :
m ∈ list.argmax f l → m ∈ l
theorem
list.argmin_mem
{α : Type u_1}
{β : Type u_2}
[decidable_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}
[decidable_linear_order β]
{f : α → β}
{l : list α} :
list.argmax f l = option.none ↔ l = list.nil
@[simp]
theorem
list.argmin_eq_none
{α : Type u_1}
{β : Type u_2}
[decidable_linear_order β]
{f : α → β}
{l : list α} :
list.argmin f l = option.none ↔ l = list.nil
theorem
list.le_argmax_of_mem
{α : Type u_1}
{β : Type u_2}
[decidable_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}
[decidable_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}
[decidable_linear_order β]
(f : α → β)
(a : α)
(l : list α) :
list.argmax f (l ++ [a]) = (list.argmax f l).cases_on (option.some a) (λ (c : α), ite (f a ≤ f c) (option.some c) (option.some a))
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 (option.some a) (λ (c : α), ite (f c ≤ f a) (option.some c) (option.some a))
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 (option.some a) (λ (c : α), ite (f c ≤ f a) (option.some a) (option.some c))
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 (option.some a) (λ (c : α), ite (f a ≤ f c) (option.some a) (option.some c))
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_1 ∈ l → f m ≤ f a_1 → list.index_of m l ≤ list.index_of a_1 l
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_1 ∈ l → f a_1 ≤ f m → list.index_of m l ≤ list.index_of a_1 l
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
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 = 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}
[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
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 = 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]