Auction.lean

View source on GitHub

Scaffolding (standard mechanism design)

Report

A player's declared bid in a direct-revelation mechanism. Each advertiser reports a center (where they're most relevant), a spread parameter sigma (how far their relevance reaches), and a bid (willingness to pay). Positivity fields keep logarithms and divisions well-formed downstream.

structure Report (E : Type*) where
  center : E
  sigma : ℝ
  bid : ℝ
  sigma_pos : 0 < sigma
  bid_pos : 0 < bid

Valuation

A player's private truth: their actual center, spread, and value. The proof keeps reports and valuations as separate types so "truthful" has a precise meaning: same center, same sigma, bid equals true value.

structure Valuation (E : Type*) where
  center : E
  trueSigma : ℝ
  trueValue : ℝ
  sigma_pos : 0 < trueSigma
  value_pos : 0 < trueValue

Auction

The full auction state: a report profile (what everyone declared) and a valuation profile (what everyone actually wants). One type parameter ι for the player set, one E for the embedding space.

structure Auction (ι : Type*) (E : Type*) where
  report : ι → Report E
  valuation : ι → Valuation E

utility

Quasilinear utility: value minus payment. Standard in mechanism design, encoded here as a definition.

def utility (_auc : Auction ι E) (_i : ι) (_x : E)
    (myValue payment : ℝ) : ℝ :=
  myValue - payment

Our composition (project-specific)

score

The scoring rule: score_i(x) = log(b_i) - ‖x - c_i‖² / σ_i². Relevance decays with squared distance from the advertiser's center, scaled by their spread. The logarithm of the bid makes this additive, which connects it to power diagrams when all sigmas are equal.

def score (r : Report E) (x : E) : ℝ :=
  Real.log r.bid - ‖x - r.center‖ ^ 2 / r.sigma ^ 2

Inspired by Lahaie & Pennock (2007), quality-weighted sponsored search.

trueVal

The Gaussian valuation model: trueVal_i(x) = v_i · exp(-‖x - c_i‖² / σ_i²). An advertiser's value for a query decays as a Gaussian with distance from their center. The peak value v_i scales the whole curve.

def trueVal (v : Valuation E) (x : E) : ℝ :=
  v.trueValue * Real.exp (-(‖x - v.center‖ ^ 2 / v.trueSigma ^ 2))

reportedVal

Same shape as trueVal, but using the reported parameters. The payment mechanism sees reportedVal. The identity score = log(reportedVal) holds unconditionally, no truthfulness required. This algebraic fact is one ingredient of the DSIC proof.

def reportedVal (r : Report E) (x : E) : ℝ :=
  r.bid * Real.exp (-(‖x - r.center‖ ^ 2 / r.sigma ^ 2))

winner

The allocation rule: at each query point x, the winner is the advertiser with the highest score.

def winner (auc : Auction ι E) (x : E) : ι :=
  -- argmax over Finset.univ of score

; Three advertisers competing for queries
(define (score center sigma bid x)
  (- (log bid) (/ (* (- x center) (- x center)) (* sigma sigma))))

(define ads
  '((0.2 0.3 5.0 "A") (0.5 0.2 2.0 "B") (0.8 0.4 8.0 "C")))

(define (get-center a) (car a))
(define (get-sigma a) (cadr a))
(define (get-bid a) (caddr a))
(define (get-name a) (cadddr a))

(define (winner ads x)
  (let loop ((rest ads) (best-score -999) (best-name ""))
    (if (null? rest) best-name
        (let ((s (score (get-center (car rest))
                        (get-sigma (car rest))
                        (get-bid (car rest)) x)))
          (if (> s best-score)
              (loop (cdr rest) s (get-name (car rest)))
              (loop (cdr rest) best-score best-name))))))

(let loop ((i 0))
  (when (<= i 10)
    (let ((x (/ i 10.0)))
      (display x) (display "  winner: ")
      (display (winner ads x)) (newline))
    (loop (+ i 1))))

import math

# Three advertisers: (center, sigma, bid)
ads = [
    {"name": "A", "center": 0.2, "sigma": 0.3, "bid": 5.0},
    {"name": "B", "center": 0.5, "sigma": 0.2, "bid": 2.0},
    {"name": "C", "center": 0.8, "sigma": 0.4, "bid": 8.0},
]

def score(r, x):
    return math.log(r["bid"]) - (x - r["center"])**2 / r["sigma"]**2

def winner(ads, x):
    scores = [(score(r, x), r["name"]) for r in ads]
    return max(scores, key=lambda s: s[0])

print(f"{'x':>4}  {'winner':>6}  {'scores (A, B, C)'}")
for i in range(11):
    x = i / 10
    s, w = winner(ads, x)
    scores = [f"{score(r, x):+.2f}" for r in ads]
    print(f"{x:.1f}   {w:>5}   [{', '.join(scores)}]")

Auction.withReport

Replace player i's report while leaving everyone's private valuations unchanged. This is how the proof models deviations: compare the original auction against auc.withReport i r' to see whether lying helps.

def Auction.withReport (auc : Auction ι E) (i : ι)
    (r' : Report E) : Auction ι E where
  report := Function.update auc.report i r'
  valuation := auc.valuation

vcgPayment

Clarke pivot: player i pays the externality they impose on others.

• welfareOthersWith: reported value of the winner (excluding i's contribution) under the current allocation.
• welfareOthersWithout: best reported value achievable for others if i were removed entirely.

Payment = without minus with. The "without" term depends only on others' reports. That invariance is one ingredient of the DSIC proof (welfareOthersWithout_invariant).

def vcgPayment (auc : Auction ι E) (i : ι) (x : E) : ℝ :=
  welfareOthersWithout auc i x - welfareOthersWith auc i x

Clarke (1971) §3, Groves (1973) Thm 2.

Connections

• Efficiency.lean — proves score = log(trueVal) under truthful reporting
• Strategyproof.lean — proves no player benefits from changing their report
• OpenGame.lean — wraps this auction in the compositional game interface
• Lahaie & Pennock (2007) — quality-weighted sponsored search, inspiration for the scoring rule
• Clarke (1971) — the pivotal mechanism and externality pricing
• Groves (1973) — incentives in teams, efficient choice rules