List.argmax under filter and map

Mathlib/Data/List/MinMax.lean characterizes argmax (List.argmax_eq_some_iff) but has no lemma relating it to filter or map. The maximizer stays the maximizer of any filter that keeps it, the choice-consistency property of selection by a score; argmax commutes with map; and it depends only on how the scores order the list, and on a list sorted by decreasing score it is the head. [UPSTREAM] candidates for that file.

Main results

• List.argmax_filter_of_mem: the maximizer of l is the maximizer of any filter of l that keeps it.
• List.argmax_map: argmax commutes with map.
• List.argmax_congr: scores that order l the same way have the same maximizer.
• List.argmax_eq_head?: on a list sorted by decreasing score the maximizer is the head.

theorem List.argmax_filter_of_mem {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : α → β} {l : List α} {m : α} {p : α → Bool} (h : m ∈ argmax f l) (hp : p m = true) : m ∈ argmax f (filter p l)

The maximizer of a list is the maximizer of any filter that keeps it.

theorem List.argmax_map {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : α → β} {δ : Type u_4} (g : δ → α) (l : List δ) : argmax f (map g l) = Option.map g (argmax (f ∘ g) l)

theorem List.argmax_congr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder β] [LinearOrder γ] {f : α → β} {l : List α} {g : α → γ} (h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → (f a ≤ f b ↔ g a ≤ g b)) : argmax f l = argmax g l

Scores that order l the same way have the same argmax.

theorem List.argmax_eq_head? {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : α → β} {l : List α} (h : Pairwise (fun (a b : α) => f b ≤ f a) l) : argmax f l = l.head?

On a list sorted by decreasing score, argmax is the head.