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.

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

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.