Proof of Proposition 5, p. 30 — $w_2>w_1$

Proved

AdDataSharing.Topics.w1_lt_w2

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

online-advertisingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1topics-api

Throughout, $\alpha\in(0,\tfrac12)$ , $0<w<C<M<2C$ , $\varphi\in(0,1)$ , $\eta_2>0$ , $\tau>1$ and $0\le\sigma<1$ (the standing assumptions of the model).

Then the two thresholds of the Topics bidding game satisfy

w_1=\frac{(1+\eta_2)-\sigma(1-\alpha)}{\tau(1+\eta_2)-\sigma(1-\alpha)}\,C\ <\ \frac{[(1+\eta_2)-\sigma]M+\alpha\sigma C}{\tau(1+\eta_2)-\sigma(1-\alpha)}=w_2 .

Because $w_1<w_2$ , the regions where both advertisers bid on $ADX_1$ ( $w\le w_1$ ) and where both bid on $ADX_2$ ( $w\ge w_2$ ) are disjoint, which gives the uniqueness part of Proposition 5.

Formalization Note The page's displayed decomposition of $w_2$ omits a factor $C$ on its first term; the stated inequality $w_2>w_1$ is the page's conclusion and does not depend on that display.

Preamble

import Mathlib
import Definitions.Def_AdDataSharing_Topics_Model

Formal statement

namespace AdDataSharing.Topics

theorem w1_lt_w2 (P : Params) (hP : P.Standing) : w₁ P < w₂ P := by sorry

end AdDataSharing.Topics

Source

Johnson, Jungbauer, Preuss, Online Advertising, Data Sharing, and Consumer Control, SSRN 3898798 (Nov. 2, 2022), Appendix p. 30, proof of Proposition 5 (w2 > w1)

Human review

Endorsed by Shuze Chen · Oct 15, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 15, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proof of Proposition 5, p. 30 — w2>w1w_2>w_1w2​>w1​

Proof of Proposition 5, p. 30 — $w_2>w_1$