EconCSLib.Foundation.OrderedGroup

Convenience lemmas for linearly ordered additive commutative groups, the standard utility/payoff type in game theory.

Typeclass convention

Throughout EconCSLib, the payoff/utility type U uses the unbundled pattern from modern Mathlib:

[AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U]

This is the unbundled equivalent of the former LinearOrderedAddCommGroup (which no longer exists as a standalone class). It provides:

• Subtraction and negation (AddCommGroup)
• Total ordering (LinearOrder)
• Order-addition compatibility: a ≤ b → a + c ≤ b + c (IsOrderedAddMonoid)

No multiplication is needed for most game theory results (Nash equilibrium, dominance, Vickrey auction). Only specific results require more:

• Quasi-linear utility v_i · x_i − p_i needs [Ring U] + [IsOrderedRing U]
• Myerson's Lemma needs ℝ (interval integration)

Standard instances: ℤ, ℚ, ℝ, and any LinearOrderedField.

Notation

We use U consistently for the payoff type throughout the library.

Key Mathlib lemmas for game theory proofs

The following Mathlib lemmas are especially useful when working with payoffs in an ordered additive group. They are not re-proved here (use the Mathlib names directly), but listed for reference:

Sign and comparison

• sub_nonneg : 0 ≤ a - b ↔ b ≤ a
• sub_nonpos : a - b ≤ 0 ↔ a ≤ b
• sub_pos : 0 < a - b ↔ b < a
• sub_neg : a - b < 0 ↔ a < b

Monotonicity of subtraction

• sub_le_sub_iff_left (a : U) : a - b ≤ a - c ↔ c ≤ b
• sub_le_sub_iff_right (c : U) : a - c ≤ b - c ↔ a ≤ b
• sub_lt_sub_iff_left (a : U) : a - b < a - c ↔ c < b

Shifting by positive/negative

• sub_lt_self (a : U) (h : 0 < b) : a - b < a
• lt_add_of_pos_right (a : U) (h : 0 < b) : a < a + b
• add_lt_of_neg_right (a : U) (h : b < 0) : a + b < a

Cancellation

• add_le_add_iff_left (a : U) : a + b ≤ a + c ↔ b ≤ c
• add_le_add_iff_right (c : U) : a + c ≤ b + c ↔ a ≤ b

Note on linarith

The linarith tactic does not work in abstract ordered additive groups — it requires LinearOrderedCommRing or similar. In proofs over abstract U, use the lemmas above directly, or use abel to normalize additive expressions before applying order lemmas.

Game-theory-specific lemmas

theorem payoff_anti_payment {U : Type u_1} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] {value price₁ price₂ : U} (h : price₁ ≤ price₂) : value - price₂ ≤ value - price₁

If paying less is better: price₁ ≤ price₂ → value - price₂ ≤ value - price₁. Useful for comparing utilities when the allocation is the same but payments differ.

theorem payoff_nonneg_iff {U : Type u_1} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] {value price : U} : 0 ≤ value - price ↔ price ≤ value

Winning is profitable iff the value exceeds the price.

theorem payoff_nonpos_iff {U : Type u_1} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] {value price : U} : value - price ≤ 0 ↔ value ≤ price

Winning is unprofitable iff the price exceeds the value.

theorem payoff_lt_of_price_lt {U : Type u_1} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] {value price₁ price₂ : U} (h : price₁ < price₂) : value - price₂ < value - price₁

Lowering the price by a positive amount strictly increases payoff.

theorem le_zero_of_add_le_self {U : Type u_1} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] {a b : U} (h : a + b ≤ a) : b ≤ 0

In a zero-sum comparison: if a + b ≤ a then b ≤ 0.

theorem nonneg_of_self_le_add {U : Type u_1} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] {a b : U} (h : a ≤ a + b) : 0 ≤ b

In a zero-sum comparison: if a ≤ a + b then 0 ≤ b.