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 WithTop α, the smallest element of l for nonempty lists, and ⊤⊤ for
[]
def
List.argAux
{α : Type u_1}
(r : α → α → Prop)
[inst : DecidableRel r]
(a : Option α)
(b : α)
:
Option α
Auxiliary definition for argmax and argmin.
Equations
- List.argAux r a b = Option.casesOn a (some b) fun c => if r b c then some b else some c
@[simp]
theorem
List.foldl_argAux_eq_none
{α : Type u_1}
(r : α → α → Prop)
[inst : DecidableRel r]
{l : List α}
{o : Option α}
:
List.foldl (List.argAux r) o l = none ↔ l = [] ∧ o = none
@[simp]
theorem
List.argAux_self
{α : Type u_1}
(r : α → α → Prop)
[inst : DecidableRel r]
(hr₀ : Irreflexive r)
(a : α)
:
List.argAux r (some a) a = some a
theorem
List.not_of_mem_foldl_argAux
{α : Type u_1}
(r : α → α → Prop)
[inst : DecidableRel r]
{l : List α}
(hr₀ : Irreflexive r)
(hr₁ : Transitive r)
{a : α}
{m : α}
{o : Option α}
:
a ∈ l → m ∈ List.foldl (List.argAux r) o l → ¬r a m
def
List.argmax
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
(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∈ 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.argAux fun b c => f c < f b) none l
def
List.argmin
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
(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∈ 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.argAux fun b c => f b < f c) none l
@[simp]
theorem
List.argmax_nil
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
(f : α → β)
:
List.argmax f [] = none
@[simp]
theorem
List.argmin_nil
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
(f : α → β)
:
List.argmin f [] = none
@[simp]
theorem
List.argmax_singleton
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
{f : α → β}
{a : α}
:
List.argmax f [a] = some a
@[simp]
theorem
List.argmin_singleton
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
{f : α → β}
{a : α}
:
List.argmin f [a] = some a
theorem
List.not_lt_of_mem_argmax
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
{f : α → β}
{l : List α}
{a : α}
{m : α}
:
a ∈ l → m ∈ List.argmax f l → ¬f m < f a
theorem
List.not_lt_of_mem_argmin
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
{f : α → β}
{l : List α}
{a : α}
{m : α}
:
a ∈ l → m ∈ List.argmin f l → ¬f a < f m
theorem
List.argmax_concat
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
(f : α → β)
(a : α)
(l : List α)
:
List.argmax f (l ++ [a]) = Option.casesOn (List.argmax f l) (some a) fun c => if f c < f a then some a else some c
theorem
List.argmin_concat
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
(f : α → β)
(a : α)
(l : List α)
:
List.argmin f (l ++ [a]) = Option.casesOn (List.argmin f l) (some a) fun c => if f a < f c then some a else some c
theorem
List.argmax_mem
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
{f : α → β}
{l : List α}
{m : α}
:
m ∈ List.argmax f l → m ∈ l
theorem
List.argmin_mem
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
{f : α → β}
{l : List α}
{m : α}
:
m ∈ List.argmin f l → m ∈ l
@[simp]
theorem
List.argmax_eq_none
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
{f : α → β}
{l : List α}
:
List.argmax f l = none ↔ l = []
@[simp]
theorem
List.argmin_eq_none
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
[inst : DecidableRel fun x x_1 => x < x_1]
{f : α → β}
{l : List α}
:
List.argmin f l = none ↔ l = []
theorem
List.le_of_mem_argmax
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder β]
{f : α → β}
{l : List α}
{a : α}
{m : α}
:
a ∈ l → m ∈ List.argmax f l → f a ≤ f m
theorem
List.le_of_mem_argmin
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder β]
{f : α → β}
{l : List α}
{a : α}
{m : α}
:
a ∈ l → m ∈ List.argmin f l → f m ≤ f a
theorem
List.argmax_cons
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder β]
(f : α → β)
(a : α)
(l : List α)
:
List.argmax f (a :: l) = Option.casesOn (List.argmax f l) (some a) fun c => if f a < f c then some c else some a
theorem
List.argmin_cons
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder β]
(f : α → β)
(a : α)
(l : List α)
:
List.argmin f (a :: l) = Option.casesOn (List.argmin f l) (some a) fun c => if f c < f a then some c else some a
theorem
List.index_of_argmax
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder β]
{f : α → β}
[inst : DecidableEq α]
{l : List α}
{m : α}
:
m ∈ List.argmax f l → ∀ {a : α}, a ∈ l → f m ≤ f a → List.indexOf m l ≤ List.indexOf a l
theorem
List.index_of_argmin
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder β]
{f : α → β}
[inst : DecidableEq α]
{l : List α}
{m : α}
:
m ∈ List.argmin f l → ∀ {a : α}, a ∈ l → f a ≤ f m → List.indexOf m l ≤ List.indexOf a l
theorem
List.mem_argmax_iff
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder β]
{f : α → β}
{l : List α}
{m : α}
[inst : DecidableEq α]
:
m ∈ List.argmax f l ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → List.indexOf m l ≤ List.indexOf a l
theorem
List.argmax_eq_some_iff
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder β]
{f : α → β}
{l : List α}
{m : α}
[inst : DecidableEq α]
:
List.argmax f l = some m ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → List.indexOf m l ≤ List.indexOf a l
theorem
List.mem_argmin_iff
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder β]
{f : α → β}
{l : List α}
{m : α}
[inst : DecidableEq α]
:
m ∈ List.argmin f l ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f m ≤ f a) ∧ ∀ (a : α), a ∈ l → f a ≤ f m → List.indexOf m l ≤ List.indexOf a l
theorem
List.argmin_eq_some_iff
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder β]
{f : α → β}
{l : List α}
{m : α}
[inst : DecidableEq α]
:
List.argmin f l = some m ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f m ≤ f a) ∧ ∀ (a : α), a ∈ l → f a ≤ f m → List.indexOf m l ≤ List.indexOf a l
def
List.maximum
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
(l : List α)
:
WithBot α
maximum l returns an WithBot α, the largest element of l for nonempty lists, and ⊥⊥ for
[]
Equations
- List.maximum l = List.argmax id l
def
List.minimum
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
(l : List α)
:
WithTop α
minimum l returns an WithTop α, the smallest element of l for nonempty lists, and ⊤⊤ for
[]
Equations
- List.minimum l = List.argmin id l
@[simp]
theorem
List.maximum_nil
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
:
List.maximum [] = ⊥
@[simp]
theorem
List.minimum_nil
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
:
List.minimum [] = ⊤
@[simp]
theorem
List.maximum_singleton
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
(a : α)
:
List.maximum [a] = ↑a
@[simp]
theorem
List.minimum_singleton
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
(a : α)
:
List.minimum [a] = ↑a
theorem
List.maximum_mem
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
{l : List α}
{m : α}
:
List.maximum l = ↑m → m ∈ l
theorem
List.minimum_mem
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
{l : List α}
{m : α}
:
List.minimum l = ↑m → m ∈ l
@[simp]
theorem
List.maximum_eq_none
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
{l : List α}
:
List.maximum l = none ↔ l = []
@[simp]
theorem
List.minimum_eq_none
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
{l : List α}
:
List.minimum l = none ↔ l = []
theorem
List.not_lt_maximum_of_mem
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
{l : List α}
{a : α}
{m : α}
:
a ∈ l → List.maximum l = ↑m → ¬m < a
theorem
List.minimum_not_lt_of_mem
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
{l : List α}
{a : α}
{m : α}
:
a ∈ l → List.minimum l = ↑m → ¬a < m
theorem
List.not_lt_maximum_of_mem'
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
{l : List α}
{a : α}
(ha : a ∈ l)
:
¬List.maximum l < ↑a
theorem
List.not_lt_minimum_of_mem'
{α : Type u_1}
[inst : Preorder α]
[inst : DecidableRel fun x x_1 => x < x_1]
{l : List α}
{a : α}
(ha : a ∈ l)
:
¬↑a < List.minimum l
theorem
List.maximum_concat
{α : Type u_1}
[inst : LinearOrder α]
(a : α)
(l : List α)
:
List.maximum (l ++ [a]) = max (List.maximum l) ↑a
theorem
List.le_maximum_of_mem
{α : Type u_1}
[inst : LinearOrder α]
{l : List α}
{a : α}
{m : α}
:
a ∈ l → List.maximum l = ↑m → a ≤ m
theorem
List.minimum_le_of_mem
{α : Type u_1}
[inst : LinearOrder α]
{l : List α}
{a : α}
{m : α}
:
a ∈ l → List.minimum l = ↑m → m ≤ a
theorem
List.le_maximum_of_mem'
{α : Type u_1}
[inst : LinearOrder α]
{l : List α}
{a : α}
(ha : a ∈ l)
:
↑a ≤ List.maximum l
theorem
List.le_minimum_of_mem'
{α : Type u_1}
[inst : LinearOrder α]
{l : List α}
{a : α}
(ha : a ∈ l)
:
List.minimum l ≤ ↑a
theorem
List.minimum_concat
{α : Type u_1}
[inst : LinearOrder α]
(a : α)
(l : List α)
:
List.minimum (l ++ [a]) = min (List.minimum l) ↑a
theorem
List.maximum_cons
{α : Type u_1}
[inst : LinearOrder α]
(a : α)
(l : List α)
:
List.maximum (a :: l) = max (↑a) (List.maximum l)
theorem
List.minimum_cons
{α : Type u_1}
[inst : LinearOrder α]
(a : α)
(l : List α)
:
List.minimum (a :: l) = min (↑a) (List.minimum l)
@[simp]
theorem
List.foldr_max_of_ne_nil
{α : Type u_1}
[inst : LinearOrder α]
[inst : OrderBot α]
{l : List α}
(h : l ≠ [])
:
↑(List.foldr max ⊥ l) = List.maximum l
theorem
List.max_le_of_forall_le
{α : Type u_1}
[inst : LinearOrder α]
[inst : OrderBot α]
(l : List α)
(a : α)
(h : ∀ (x : α), x ∈ l → x ≤ a)
:
List.foldr max ⊥ l ≤ a
theorem
List.le_max_of_le
{α : Type u_1}
[inst : LinearOrder α]
[inst : OrderBot α]
{l : List α}
{a : α}
{x : α}
(hx : x ∈ l)
(h : a ≤ x)
:
a ≤ List.foldr max ⊥ l
@[simp]
theorem
List.foldr_min_of_ne_nil
{α : Type u_1}
[inst : LinearOrder α]
[inst : OrderTop α]
{l : List α}
(h : l ≠ [])
:
↑(List.foldr min ⊤ l) = List.minimum l
theorem
List.le_min_of_forall_le
{α : Type u_1}
[inst : LinearOrder α]
[inst : OrderTop α]
(l : List α)
(a : α)
(h : ∀ (x : α), x ∈ l → a ≤ x)
:
a ≤ List.foldr min ⊤ l
theorem
List.min_le_of_le
{α : Type u_1}
[inst : LinearOrder α]
[inst : OrderTop α]
(l : List α)
(a : α)
{x : α}
(hx : x ∈ l)
(h : x ≤ a)
:
List.foldr min ⊤ l ≤ a