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_nonempty — nonempty on nonempty input (via exists_max_image).
• argmax_comp_strictMono — invariance under strictly monotone rescaling.

def Finset.argmax {α : Type u_1} {β : Type u_2} [LinearOrder β] (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}

@[simp]

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

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

theorem Finset.argmax_nonempty {α : Type u_1} {β : Type u_2} [LinearOrder β] {s : Finset α} {f : α → β} (hs : s.Nonempty) : (s.argmax f).Nonempty

def Finset.argmin {α : Type u_1} {β : Type u_2} [LinearOrder β] (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_argmin {α : Type u_1} {β : Type u_2} [LinearOrder β] {s : Finset α} {f : α → β} {a : α} : a ∈ s.argmin f ↔ a ∈ s ∧ ∀ b ∈ s, f a ≤ f b

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

theorem Finset.argmin_nonempty {α : Type u_1} {β : Type u_2} [LinearOrder β] {s : Finset α} {f : α → β} (hs : s.Nonempty) : (s.argmin f).Nonempty

theorem Finset.argmin_eq_argmax_toDual {α : Type u_1} {β : Type u_2} [LinearOrder β] {s : Finset α} {f : α → β} : s.argmin f = s.argmax (⇑OrderDual.toDual ∘ f)

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

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

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

Scores that order s oppositely swap argmin and argmax.

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

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

theorem Finset.argmax_eq_argmax_of_support {α : Type u_1} {β : Type u_2} [LinearOrder β] {s : Finset α} {f : α → β} [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

The argmax of a score that is positive on a nonempty t ⊆ s and zero on the rest of s is the argmax over t.

theorem Finset.argmax_comp_strictMono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder β] [LinearOrder γ] {s : Finset α} {f : α → β} {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.

@[simp]

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

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

Membership in an argmax over univ, through a surjection: a maximizes φ ∘ e iff e a maximizes φ. Collapses argmax over a function space to argmax over values when the objective factors through evaluation.

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)

Membership in the argmax of a coordinatewise sum over a finite pi type: g maximizes ∑ i, φ i (g i) iff every coordinate maximizes its own summand. The additive-separability workhorse for best responses in games.

theorem Finset.fold_max_attained {α : Type u_1} {β : Type u_2} [LinearOrder β] (s : Finset α) (f : α → β) (b : β) : fold max b f s = b ∨ ∃ x ∈ s, fold max b f s = f x

A Finset.fold max is attained either at the initial value or at some element. [UPSTREAM] candidate alongside argmax.