Uniform-over-argmax choice rule

PMF.uniformOfArgmax score is the PMF uniform over the score-maximal elements (Finset.argmax). It is the hard-choice sibling of PMF.softmax (Core/Probability/Softmax.lean): as the inverse temperature inside a softmax score grows without bound, softmax mass concentrates on the argmax set (Core/Probability/SoftmaxLimits.lean proves the ℝ-level limit). Iterated-best-response models ([Fra11]) use this rule where RSA ([FG12]) uses softmax.

Main definitions

• PMF.uniformOfArgmax score — uniform PMF over Finset.univ.argmax score.

Main statements

• support_uniformOfArgmax — the support is the argmax set.
• uniformOfArgmax_apply_pos_iff — positive mass iff score-maximal.
• uniformOfArgmax_comp_strictMono — invariance under strictly monotone rescaling of the score (inverse-temperature invariance).

Definition

noncomputable def PMF.uniformOfArgmax {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [LinearOrder β] (score : α → β) : PMF α

The argmax choice rule: uniform distribution over the score-maximal elements. Hard-choice counterpart of PMF.softmax; the selection rule of iterated-best-response models ([Fra11]).

Equations

• PMF.uniformOfArgmax score = PMF.uniformOfFinset (Finset.univ.argmax score) ⋯

API

@[simp]

theorem PMF.support_uniformOfArgmax {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [LinearOrder β] (score : α → β) : (uniformOfArgmax score).support = ↑(Finset.univ.argmax score)

The support of the argmax choice rule is the argmax set.

theorem PMF.uniformOfArgmax_apply_pos_iff {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [LinearOrder β] (score : α → β) (a : α) : 0 < (uniformOfArgmax score) a ↔ ∀ (b : α), score b ≤ score a

The argmax choice rule assigns positive mass exactly to the score-maximal elements.

theorem PMF.uniformOfArgmax_apply_of_max {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [LinearOrder β] (score : α → β) (a : α) (ha : ∀ (b : α), score b ≤ score a) : (uniformOfArgmax score) a = (↑(Finset.univ.argmax score).card)⁻¹

Mass of a score-maximal element: one over the size of the argmax set.

theorem PMF.uniformOfArgmax_apply_of_not_max {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [LinearOrder β] (score : α → β) (a : α) (ha : ¬∀ (b : α), score b ≤ score a) : (uniformOfArgmax score) a = 0

Non-maximal elements get zero mass.

theorem PMF.uniformOfArgmax_comp_strictMono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Nonempty α] [LinearOrder β] [LinearOrder γ] (score : α → β) {g : β → γ} (hg : StrictMono g) : uniformOfArgmax (g ∘ score) = uniformOfArgmax score

The argmax choice rule is invariant under strictly monotone rescaling of the score: changing the inverse temperature does not move the hard choice.

theorem PMF.uniformOfArgmax_const {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [LinearOrder β] (c : β) : (uniformOfArgmax fun (x : α) => c) = uniformOfFintype α

A constant score yields the uniform distribution.