Lean declarations

theorem List.exists_argMax_on EconCSLib @ cef01c7, EconCSLib.Foundation.Argmax

theorem exists_argMax_on [TotalPreorder Y] (f : X → Y)
    (head : X) (tail : List X) :
    ∃ m, m ∈ head :: tail ∧ ∀ x ∈ head :: tail, f x ≤ f m

def List.argMaxOn EconCSLib @ cef01c7, EconCSLib.Foundation.Argmax

def argMaxOn [TotalPreorder Y] [DecidableLE Y] (f : X → Y)
    (head : X) (tail : List X) : X :=
  tail.foldl (fun a z => if f a ≤ f z then z else a) head

theorem List.argMaxOn_mem EconCSLib @ cef01c7, EconCSLib.Foundation.Argmax

The chosen maximizer is a member of the list.

theorem argMaxOn_mem [TotalPreorder Y] [DecidableLE Y] (f : X → Y)
    (head : X) (tail : List X) :
    argMaxOn f head tail ∈ head :: tail

theorem List.argMaxOn_ge EconCSLib @ cef01c7, EconCSLib.Foundation.Argmax

Soundness: every element's `f`-image is `≤` the chosen maximizer's.

theorem argMaxOn_ge [TotalPreorder Y] [DecidableLE Y] (f : X → Y)
    (head : X) (tail : List X) :
    ∀ x ∈ head :: tail, f x ≤ f (argMaxOn f head tail)

theorem List.le_argMaxOn_head EconCSLib @ cef01c7, EconCSLib.Foundation.Argmax

The argmax achieves at least the head's value.

theorem le_argMaxOn_head [TotalPreorder Y] [DecidableLE Y] (f : X → Y)
    (head : X) (tail : List X) :
    f head ≤ f (argMaxOn f head tail)

Modules: EconCSLib.Foundation.Argmax

Argmax of a List under a Total Preorder

For a function f : α → β valued in a TotalPreorder β and a non-empty list head :: tail : List α, some element of the list maximizes f: $$ \exists m \in \operatorname{head} :: \operatorname{tail},\; \forall x \in \operatorname{head} :: \operatorname{tail},\; f(x) \le f(m). $$

The proof is by induction on tail, comparing the current maximum against the new head via TotalPreorder.le_total.

From the existence statement a noncomputable choice List.argMaxOn f head tail picks a witnessing maximizer. Its API:

argMaxOn_mem -- the chosen element lies in the list.
argMaxOn_ge -- the chosen element is ≥ every list element in f-value.
le_argMaxOn_head -- specialization: the head's value is ≤ the chosen element's value.

The variant exists because Mathlib's List.argmax is computable but requires [LinearOrder], which is too strong for ranking outcomes that may be indifferent (the typical situation when a player's payoffs are equal across distinct continuations). The intended consumer is ExtensiveGame.BackwardInduction, where finite game trees are evaluated by recursively picking an argmax of children.

References

[MSZ, Chapter 3] Maschler, Solan, and Zamir, Game Theory. Backward induction on finite extensive games.

Argmax of a List under a Total Preorder

References

Also in