The argmax set of a function on a finset

Finset.argmax s f is the finset of elements of s at which f attains its maximum over s. Mathlib has only the tie-breaking List.argmax : List α → Option α; the set-valued form is the natural companion of Finset.max' and Finset.exists_max_image, and the carrier for argmax correspondences (set-valued best responses) in game-theoretic consumers.

[UPSTREAM] candidate: Mathlib.Data.Finset.Max.

Main definitions

• Finset.argmax s f — the score-maximal elements of s.
• Finset.argmin s f — the score-minimal elements of s.

Main statements

• mem_argmax — membership characterization (simp normal form).
• argmax_eq_singleton_iff — a sole maximizer strictly beats every other element.
• StrictAntiOn.argmin_eq_singleton — a strictly antitone score is minimized at the greatest element.
• argmax_nonempty — nonempty on nonempty input, in a total preorder.
• argmax_comp_strictMono — invariance under strictly monotone rescaling.

Implementation notes

As for List.argmax, the definition asks only for a preorder with decidable ≤, not a linear order, and the existence and uniqueness lemmas ask for totality on top. A score type whose LinearOrder decides ≤ classically, such as Lex (Fin n → ℕ), can then be scored under a computable DecidableLE instance and evaluated by decide. In a preorder that is not total, argmax is the set of elements at which f is greatest, which can be empty, not the set of MaximalFor elements. The lemmas stated for linear orders take the order's own decidability, so they do not apply under such a separate instance.

def Finset.argmax {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLE β] (s : Finset α) (f : α → β) : Finset α

The elements of s at which f attains its maximum over s.

Equations

• s.argmax f = {a ∈ s | ∀ b ∈ s, f b ≤ f a}

def Finset.argmin {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLE β] (s : Finset α) (f : α → β) : Finset α

The elements of s at which f attains its minimum over s.

Equations

• s.argmin f = {a ∈ s | ∀ b ∈ s, f a ≤ f b}

@[simp]

theorem Finset.mem_argmax {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} {a : α} [Preorder β] [DecidableLE β] : a ∈ s.argmax f ↔ a ∈ s ∧ ∀ b ∈ s, f b ≤ f a

@[simp]

theorem Finset.mem_argmin {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} {a : α} [Preorder β] [DecidableLE β] : a ∈ s.argmin f ↔ a ∈ s ∧ ∀ b ∈ s, f a ≤ f b

theorem Finset.argmax_subset {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [Preorder β] [DecidableLE β] : s.argmax f ⊆ s

theorem Finset.argmin_subset {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [Preorder β] [DecidableLE β] : s.argmin f ⊆ s

@[simp]

theorem Finset.argmax_empty {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder β] [DecidableLE β] : ∅.argmax f = ∅

@[simp]

theorem Finset.argmin_empty {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder β] [DecidableLE β] : ∅.argmin f = ∅

theorem Finset.argmax_eq_self_of_forall_le {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [Preorder β] [DecidableLE β] (h : ∀ a ∈ s, ∀ b ∈ s, f b ≤ f a) : s.argmax f = s

theorem Finset.argmin_eq_self_of_forall_le {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [Preorder β] [DecidableLE β] (h : ∀ a ∈ s, ∀ b ∈ s, f a ≤ f b) : s.argmin f = s

A score that is constant on s has all of s as argmin.

@[simp]

theorem Finset.argmax_const {α : Type u_1} {β : Type u_2} {s : Finset α} [Preorder β] [DecidableLE β] (c : β) : (s.argmax fun (x : α) => c) = s

@[simp]

theorem Finset.argmin_const {α : Type u_1} {β : Type u_2} {s : Finset α} [Preorder β] [DecidableLE β] (c : β) : (s.argmin fun (x : α) => c) = s

theorem Finset.argmin_eq_argmax_of_le_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {f : α → β} [Preorder β] [DecidableLE β] [Preorder γ] [DecidableLE γ] {f' : α → γ} (h : ∀ a ∈ s, ∀ b ∈ s, f a ≤ f b ↔ f' b ≤ f' a) : s.argmin f = s.argmax f'

theorem Finset.mem_argmax_comp_surjective {α : Type u_1} {β : Type u_2} [Preorder β] [DecidableLE β] {α' : Type u_4} [Fintype α] [Fintype α'] {e : α → α'} (he : Function.Surjective e) (φ : α' → β) {a : α} : a ∈ univ.argmax (φ ∘ e) ↔ e a ∈ univ.argmax φ

theorem Finset.argmax_eq_singleton_iff {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} {a : α} [Preorder β] [DecidableLE β] : s.argmax f = {a} ↔ a ∈ s ∧ ∀ b ∈ s, b ≠ a → f b < f a

The argmax is the singleton {a} iff a ∈ s beats every other element of s.

theorem Finset.argmin_eq_singleton_iff {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} {a : α} [Preorder β] [DecidableLE β] : s.argmin f = {a} ↔ a ∈ s ∧ ∀ b ∈ s, b ≠ a → f a < f b

The argmin is the singleton {a} iff a ∈ s beats every other element of s.

theorem StrictAntiOn.argmin_eq_singleton {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} {a : α} [Preorder β] [DecidableLE β] [PartialOrder α] (hf : StrictAntiOn f ↑s) (ha : IsGreatest (↑s) a) : s.argmin f = {a}

A score strictly antitone on s is minimized exactly at the greatest element of s.

theorem Finset.argmax_nonempty {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [Preorder β] [DecidableLE β] [Std.Total fun (x1 x2 : β) => x1 ≤ x2] (hs : s.Nonempty) : (s.argmax f).Nonempty

In a total preorder, a nonempty finset has a maximizer.

theorem Finset.argmin_nonempty {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [Preorder β] [DecidableLE β] [Std.Total fun (x1 x2 : β) => x2 ≤ x1] (hs : s.Nonempty) : (s.argmin f).Nonempty

In a total preorder, a nonempty finset has a minimizer.

theorem Finset.mem_argmax_piFinset_sum {ι : Type u_4} [Fintype ι] [DecidableEq ι] {κ : ι → Type u_5} {K : Type u_6} [AddCommMonoid K] [PartialOrder K] [IsOrderedCancelAddMonoid K] [DecidableLE K] (s : (i : ι) → Finset (κ i)) (φ : (i : ι) → κ i → K) {g : (i : ι) → κ i} : (g ∈ (Fintype.piFinset s).argmax fun (g' : (a : ι) → κ a) => ∑ i : ι, φ i (g' i)) ↔ ∀ (i : ι), g i ∈ (s i).argmax (φ i)

theorem Finset.mem_argmin_piFinset_sum {ι : Type u_4} [Fintype ι] [DecidableEq ι] {κ : ι → Type u_5} {K : Type u_6} [AddCommMonoid K] [PartialOrder K] [IsOrderedCancelAddMonoid K] [DecidableLE K] (s : (i : ι) → Finset (κ i)) (φ : (i : ι) → κ i → K) {g : (i : ι) → κ i} : (g ∈ (Fintype.piFinset s).argmin fun (g' : (a : ι) → κ a) => ∑ i : ι, φ i (g' i)) ↔ ∀ (i : ι), g i ∈ (s i).argmin (φ i)

theorem Finset.argmax_eq_argmax_of_support {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [LinearOrder β] [Zero β] {t : Finset α} (hts : t ⊆ s) (hne : t.Nonempty) (hpos : ∀ a ∈ t, 0 < f a) (hzero : ∀ a ∈ s, a ∉ t → f a = 0) : s.argmax f = t.argmax f

theorem Finset.argmax_comp_strictMono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {f : α → β} [LinearOrder β] [LinearOrder γ] {g : β → γ} (hg : StrictMono g) : s.argmax (g ∘ f) = s.argmax f

The argmax set is invariant under strictly monotone rescaling of the score — inverse-temperature changes do not move the argmax.

theorem Finset.mem_argmax_pi_sum {ι : Type u_4} [Fintype ι] [DecidableEq ι] {Y : ι → Type u_5} [(i : ι) → Fintype (Y i)] {K : Type u_6} [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] (φ : (i : ι) → Y i → K) {g : (i : ι) → Y i} : (g ∈ univ.argmax fun (g' : (i : ι) → Y i) => ∑ i : ι, φ i (g' i)) ↔ ∀ (i : ι), g i ∈ univ.argmax (φ i)