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 a WithTop α, the smallest element of l for nonempty lists, and ⊤ for
[]
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)
[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)
[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)
[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}
[Preorder β]
[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 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}
[Preorder β]
[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 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}
[Preorder β]
[DecidableRel fun (x x_1 : β) => x < x_1]
(f : α → β)
:
List.argmax f [] = none
@[simp]
theorem
List.argmin_nil
{α : Type u_1}
{β : Type u_2}
[Preorder β]
[DecidableRel fun (x x_1 : β) => x < x_1]
(f : α → β)
:
List.argmin f [] = none
@[simp]
theorem
List.argmax_singleton
{α : Type u_1}
{β : Type u_2}
[Preorder β]
[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}
[Preorder β]
[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}
[Preorder β]
[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}
[Preorder β]
[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}
[Preorder β]
[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}
[Preorder β]
[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}
[Preorder β]
[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}
[Preorder β]
[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}
[Preorder β]
[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}
[Preorder β]
[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}
[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}
[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}
[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}
[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}
[LinearOrder β]
{f : α → β}
[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}
[LinearOrder β]
{f : α → β}
[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}
[LinearOrder β]
{f : α → β}
{l : List α}
{m : α}
[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}
[LinearOrder β]
{f : α → β}
{l : List α}
{m : α}
[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}
[LinearOrder β]
{f : α → β}
{l : List α}
{m : α}
[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}
[LinearOrder β]
{f : α → β}
{l : List α}
{m : α}
[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}
[Preorder α]
[DecidableRel fun (x x_1 : α) => x < x_1]
(l : List α)
:
WithBot α
maximum l returns a WithBot α, the largest element of l for nonempty lists, and ⊥ for
[]
Equations
- l.maximum = List.argmax id l
def
List.minimum
{α : Type u_1}
[Preorder α]
[DecidableRel fun (x x_1 : α) => x < x_1]
(l : List α)
:
WithTop α
minimum l returns a WithTop α, the smallest element of l for nonempty lists, and ⊤ for
[]
Equations
- l.minimum = List.argmin id l
@[simp]
@[simp]
@[simp]
theorem
List.maximum_singleton
{α : Type u_1}
[Preorder α]
[DecidableRel fun (x x_1 : α) => x < x_1]
(a : α)
:
[a].maximum = ↑a
@[simp]
theorem
List.minimum_singleton
{α : Type u_1}
[Preorder α]
[DecidableRel fun (x x_1 : α) => x < x_1]
(a : α)
:
[a].minimum = ↑a
theorem
List.maximum_mem
{α : Type u_1}
[Preorder α]
[DecidableRel fun (x x_1 : α) => x < x_1]
{l : List α}
{m : α}
:
theorem
List.minimum_mem
{α : Type u_1}
[Preorder α]
[DecidableRel fun (x x_1 : α) => x < x_1]
{l : List α}
{m : α}
:
@[simp, deprecated List.maximum_eq_bot]
theorem
List.maximum_eq_none
{α : Type u_1}
[Preorder α]
[DecidableRel fun (x x_1 : α) => x < x_1]
{l : List α}
:
@[simp, deprecated List.minimum_eq_top]
theorem
List.minimum_eq_none
{α : Type u_1}
[Preorder α]
[DecidableRel fun (x x_1 : α) => x < x_1]
{l : List α}
:
theorem
List.not_lt_maximum_of_mem'
{α : Type u_1}
[Preorder α]
[DecidableRel fun (x x_1 : α) => x < x_1]
{l : List α}
{a : α}
(ha : a ∈ l)
:
theorem
List.not_lt_minimum_of_mem'
{α : Type u_1}
[Preorder α]
[DecidableRel fun (x x_1 : α) => x < x_1]
{l : List α}
{a : α}
(ha : a ∈ l)
:
theorem
List.le_maximum_of_mem'
{α : Type u_1}
[LinearOrder α]
{l : List α}
{a : α}
(ha : a ∈ l)
:
↑a ≤ l.maximum
theorem
List.minimum_le_of_mem'
{α : Type u_1}
[LinearOrder α]
{l : List α}
{a : α}
(ha : a ∈ l)
:
l.minimum ≤ ↑a
theorem
List.maximum_le_of_forall_le
{α : Type u_1}
[LinearOrder α]
{l : List α}
{b : WithBot α}
(h : ∀ (a : α), a ∈ l → ↑a ≤ b)
:
l.maximum ≤ b
theorem
List.le_minimum_of_forall_le
{α : Type u_1}
[LinearOrder α]
{l : List α}
{b : WithTop α}
(h : ∀ (a : α), a ∈ l → b ≤ ↑a)
:
b ≤ l.minimum
theorem
List.maximum_ne_bot_of_length_pos
{α : Type u_1}
[LinearOrder α]
{l : List α}
(h : 0 < l.length)
:
theorem
List.minimum_ne_top_of_length_pos
{α : Type u_1}
[LinearOrder α]
{l : List α}
(h : 0 < l.length)
:
The maximum value in a non-empty List.
Equations
- List.maximum_of_length_pos h = l.maximum.unbot ⋯
The minimum value in a non-empty List.
Equations
@[simp]
theorem
List.coe_maximum_of_length_pos
{α : Type u_1}
[LinearOrder α]
{l : List α}
(h : 0 < l.length)
:
↑(List.maximum_of_length_pos h) = l.maximum
@[simp]
theorem
List.coe_minimum_of_length_pos
{α : Type u_1}
[LinearOrder α]
{l : List α}
(h : 0 < l.length)
:
↑(List.minimum_of_length_pos h) = l.minimum
@[simp]
theorem
List.le_maximum_of_length_pos_iff
{α : Type u_1}
[LinearOrder α]
{l : List α}
{b : α}
(h : 0 < l.length)
:
b ≤ List.maximum_of_length_pos h ↔ ↑b ≤ l.maximum
@[simp]
theorem
List.minimum_of_length_pos_le_iff
{α : Type u_1}
[LinearOrder α]
{l : List α}
{b : α}
(h : 0 < l.length)
:
List.minimum_of_length_pos h ≤ b ↔ l.minimum ≤ ↑b
theorem
List.maximum_of_length_pos_mem
{α : Type u_1}
[LinearOrder α]
{l : List α}
(h : 0 < l.length)
:
theorem
List.minimum_of_length_pos_mem
{α : Type u_1}
[LinearOrder α]
{l : List α}
(h : 0 < l.length)
:
theorem
List.le_maximum_of_length_pos_of_mem
{α : Type u_1}
[LinearOrder α]
{l : List α}
{a : α}
(h : a ∈ l)
(w : 0 < l.length)
:
theorem
List.minimum_of_length_pos_le_of_mem
{α : Type u_1}
[LinearOrder α]
{l : List α}
{a : α}
(h : a ∈ l)
(w : 0 < l.length)
:
theorem
List.getElem_le_maximum_of_length_pos
{α : Type u_1}
[LinearOrder α]
{l : List α}
{i : ℕ}
(w : i < l.length)
(h : optParam (0 < l.length) ⋯)
:
l[i] ≤ List.maximum_of_length_pos h
theorem
List.minimum_of_length_pos_le_getElem
{α : Type u_1}
[LinearOrder α]
{l : List α}
{i : ℕ}
(w : i < l.length)
(h : optParam (0 < l.length) ⋯)
:
List.minimum_of_length_pos h ≤ l[i]
@[simp]
theorem
List.foldr_max_of_ne_nil
{α : Type u_1}
[LinearOrder α]
[OrderBot α]
{l : List α}
(h : l ≠ [])
:
↑(List.foldr max ⊥ l) = l.maximum
theorem
List.max_le_of_forall_le
{α : Type u_1}
[LinearOrder α]
[OrderBot α]
(l : List α)
(a : α)
(h : ∀ (x : α), x ∈ l → x ≤ a)
:
List.foldr max ⊥ l ≤ a
theorem
List.le_max_of_le
{α : Type u_1}
[LinearOrder α]
[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}
[LinearOrder α]
[OrderTop α]
{l : List α}
(h : l ≠ [])
:
↑(List.foldr min ⊤ l) = l.minimum
theorem
List.le_min_of_forall_le
{α : Type u_1}
[LinearOrder α]
[OrderTop α]
(l : List α)
(a : α)
(h : ∀ (x : α), x ∈ l → a ≤ x)
:
a ≤ List.foldr min ⊤ l
theorem
List.min_le_of_le
{α : Type u_1}
[LinearOrder α]
[OrderTop α]
(l : List α)
(a : α)
{x : α}
(hx : x ∈ l)
(h : x ≤ a)
:
List.foldr min ⊤ l ≤ a