GaussianOptimality.lean

View source on GitHub

trueVal_positive

The Gaussian value function is strictly positive everywhere: trueValue > 0 (the valuation peak) and exp(·) > 0 make the product positive. A small lemma, but it confirms the model stays in the positive reals where log is well-defined.

theorem trueVal_positive (v : Valuation E) (x : E) :
    0 < trueVal v x

gaussian_optimality

Under truthful reporting, the VCG allocation maximizes integrated welfare over all allocation rules. This is a direct application of integral_efficiency — the Gaussian-specific content is already baked into the definitions.

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

gaussian_vcg_weakly_dominates

The headline result, bundling three properties in one conjunction:

1. Welfare-optimality: no allocation rule achieves higher integrated welfare.
2. No profitable deviation at the truthful profile: when all players are truthful, no single player benefits from deviating. This is weaker than full DSIC (which only requires player i to be truthful — see vcg_dsic in Strategyproof.lean), but stronger than standard Nash because it quantifies over all report deviations without depending on a continuation.
3. Allocation efficiency: the equilibrium allocation is pointwise welfare-maximizing.

theorem gaussian_vcg_weakly_dominates
    (auc : Auction ι E) (μ : QueryMeasure E)
    (htruth : allTruthful auc) :
    -- 1. No allocation rule does better
    (∀ rule, welfareOfRule auc (winner auc) μ ≥
             welfareOfRule auc rule μ) ∧
    -- 2. No advertiser benefits from deviating
    (∀ i x r', playerUtility auc i x ≥
               playerUtility (auc.withReport i r') i x) ∧
    -- 3. Equilibrium allocation is pointwise optimal
    (∀ x j, trueVal (auc.valuation (winner auc x)) x ≥
            trueVal (auc.valuation j) x)

Together: the allocation is optimal within the model, the equilibrium achieves it, and no player wants to deviate.

What's Gaussian-specific vs. inherited

Most of the heavy lifting is already done in earlier files. The Gaussian-specific content here is narrow: trueVal_positive confirms the model stays in positive reals (where log is monotone), and the capstone bundles results that were proved generically. The Gaussian valuation shape matters because it makes score = log(value) a clean algebraic identity — a different valuation model would need a different bridge theorem in Efficiency.lean.

Why this matters for economists

The Gaussian decay model is the natural choice when relevance decreases with distance in embedding space, the rate of decrease is advertiser-specific, and willingness to pay scales the whole curve. Under these assumptions, no allocation rule within the model can achieve higher integrated welfare. The only room for improvement is in the choice of embedding space itself, which is outside the auction's scope. For the economic argument, see the Vector Space series.

Connections

• IntegralEfficiency.lean — supplies welfare-optimality
• Strategyproof.lean — supplies DSIC
• Efficiency.lean — supplies pointwise welfare maximization
• OpenGame.lean — the compositional game theory connection
• Groves (1973) — efficient choice rule = argmax of values
• Green & Laffont (1977) — VCG is the only efficient DSIC mechanism
• Aurenhammer (1987) — power diagram geometry