IntegralEfficiency.lean

View source on GitHub

welfareOfRule

Integrated welfare of an allocation rule under the monotone functional μ. The rule maps each query to a winning advertiser; welfare is μ.integrate applied to the winner's valuation function.

def welfareOfRule (auc : Auction ι E) (rule : E → ι)
    (μ : QueryMeasure E) : ℝ :=
  μ.integrate (fun x => trueVal (auc.valuation (rule x)) x)

integral_efficiency

The main result. Under truthful reporting, for any allocation rule rule : E → ι:

μ.integrate(trueVal(winner(·), ·)) ≥ μ.integrate(trueVal(rule(·), ·))

The proof is one line: apply integral_mono from QueryMeasure to the pointwise bound from winner_maximizes_welfare.

theorem integral_efficiency
    (auc : Auction ι E) (μ : QueryMeasure E)
    (htruth : allTruthful auc) :
    ∀ (rule : E → ι),
      welfareOfRule auc (fun x => winner auc x) μ ≥
        welfareOfRule auc rule μ

Groves (1973) Thm 1: efficient choice rule = argmax of values. Standard measure theory: pointwise domination implies integral domination.

; Pointwise domination lifts to any monotone functional
(define xs '(0.1 0.3 0.5 0.7 0.9))

(define (trueVal c s v x)
  (* v (exp (- (/ (* (- x c) (- x c)) (* s s))))))

(define (winner-val x)
  (max (trueVal 0.3 0.3 5.0 x)
       (trueVal 0.7 0.25 4.0 x)))

(define (alt-val x) (trueVal 0.3 0.3 5.0 x))

(display "Pointwise: winner >= alt") (newline)
(for-each (lambda (x)
  (display "  x=") (display x)
  (display "  w=") (display (round (* (winner-val x) 100)))
  (display "  a=") (display (round (* (alt-val x) 100)))
  (display "  ") (display (>= (winner-val x) (alt-val x)))
  (newline)) xs)

(newline) (display "Integrated:") (newline)
(let ((ws (map winner-val xs)) (as (map alt-val xs)))
  (display "  sum: ") (display (>= (apply + ws) (apply + as))) (newline)
  (display "  max: ") (display (>= (apply max ws) (apply max as))) (newline)
  (display "  pt:  ") (display (>= (winner-val 0.5) (alt-val 0.5))) (newline))

import math

xs = [0.1, 0.3, 0.5, 0.7, 0.9]

ads = [
    {"c": 0.3, "s": 0.3, "v": 5.0},
    {"c": 0.7, "s": 0.25, "v": 4.0},
]

def trueVal(a, x):
    return a["v"] * math.exp(-(x - a["c"])**2 / a["s"]**2)

def winner_val(x):
    return max(trueVal(a, x) for a in ads)

def alt_val(x):  # always pick advertiser 0
    return trueVal(ads[0], x)

print("Pointwise: winner >= alt at every x")
for x in xs:
    w, a = winner_val(x), alt_val(x)
    print(f"  x={x}  winner={w:.3f}  alt={a:.3f}  {w >= a}")

# Three monotone functionals
mu_sum  = lambda f: sum(f(x) for x in xs)
mu_max  = lambda f: max(f(x) for x in xs)
mu_pt   = lambda f: f(0.5)

print("\nIntegrated: winner >= alt under every functional")
for name, mu in [("sum", mu_sum), ("max", mu_max), ("point", mu_pt)]:
    w, a = mu(winner_val), mu(alt_val)
    print(f"  {name:6s}  winner={w:.3f}  alt={a:.3f}  {w >= a}")

integral_efficiency_pointwise_unique

If an alternative allocation rule achieves the same integrated welfare as the winner rule, the two must agree at every query point. This requires an extra hypothesis beyond monotonicity: a faithfulness property saying that pointwise ≥ with equal integrals implies pointwise equality. The theorem takes this as an explicit precondition (hstrict).

theorem integral_efficiency_pointwise_unique
    -- requires: hstrict (faithfulness of the integral)
    -- if welfareOfRule(winner) = welfareOfRule(rule), then
    ∀ x, trueVal (auc.valuation (winner auc x)) x =
         trueVal (auc.valuation (rule x)) x

Without Mathlib's measure theory, pointwise equality is assumed directly via hstrict rather than derived from measure-theoretic properties. In general, pointwise ≥ with equal integrals only gives a.e. equality; pointwise equality is a strictly stronger demand.

Connections

• Efficiency.lean — supplies the pointwise bound winner_maximizes_welfare
• Axioms.lean — supplies QueryMeasure.integral_mono
• GaussianOptimality.lean — composes this with strategyproofness for the capstone
• Groves (1973) — efficient choice rule = argmax of values