EconCSLib.Foundation.Argmax

Argmax helpers for total preorders on non-empty lists.

Why a bespoke version

Mathlib's List.argmax / Finset.argmax require [LinearOrder] (antisymmetry). The backward-induction proof in ExtensiveGame.BackwardInduction only needs [TotalPreorder] (no antisymmetry). This file closes that gap with a computable argmax: a left fold that keeps the running maximizer, needing only a decidable comparison [DecidableLE] for the fold and [TotalPreorder] for correctness.

Main definitions

• List.exists_argMax_on — some element of head :: tail maximizes f (pure existence, [TotalPreorder] only)
• List.argMaxOn — chosen such element, computed by a fold ([TotalPreorder] + [DecidableLE])
• List.argMaxOn_mem — the chosen element is in the list
• List.argMaxOn_ge — every element's f-image is ≤ the chosen one's

theorem List.exists_argMax_on {X : Type u_1} {Y : Type u_2} [TotalPreorder Y] (f : X → Y) (head : X) (tail : List X) : ∃ (m : X), m ∈ head :: tail ∧ ∀ (x : X), x ∈ head :: tail → f x ≤ f m

Existence of an argmax on a non-empty list under a total preorder. Since the preorder may lack antisymmetry, ties are allowed — we only claim existence of some maximizer, not uniqueness.

def List.argMaxOn {X : Type u_1} {Y : Type u_2} [TotalPreorder Y] [DecidableLE Y] (f : X → Y) (head : X) (tail : List X) : X

A chosen maximizer of f on the non-empty list head :: tail, computed by a left fold that keeps the running maximizer (ties keep the later element). Computable: the fold needs only a decidable comparison [DecidableLE Y]; correctness (argMaxOn_mem / argMaxOn_ge) needs the total preorder.

Equations

• List.argMaxOn f head tail = List.foldl (fun (a z : X) => if f a ≤ f z then z else a) head tail

theorem List.argMaxOn_mem {X : Type u_1} {Y : Type u_2} [TotalPreorder Y] [DecidableLE Y] (f : X → Y) (head : X) (tail : List X) : argMaxOn f head tail ∈ head :: tail

The chosen maximizer is a member of the list.

theorem List.argMaxOn_ge {X : Type u_1} {Y : Type u_2} [TotalPreorder Y] [DecidableLE Y] (f : X → Y) (head : X) (tail : List X) (x : X) : x ∈ head :: tail → f x ≤ f (argMaxOn f head tail)

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

theorem List.le_argMaxOn_head {X : Type u_1} {Y : Type u_2} [TotalPreorder Y] [DecidableLE Y] (f : X → Y) (head : X) (tail : List X) : f head ≤ f (argMaxOn f head tail)

The argmax achieves at least the head's value.