Probability

Motivation

Bayesian persuasion studies a sender who observes a state of the world and commits in advance to a randomized disclosure rule, in order to influence the action of a receiver who updates her belief by Bayes' rule. Since Kamenica and Gentzkow (2011) the model has been applied to platform design, recommendation systems, queue information and rating systems. Almost all of this theory assumes the receiver is an expected-utility maximizer, so that her payoff from each action is linear in her belief.

Many receivers are not. A customer who joins a queue only if the mean of her waiting time plus a multiple of its standard deviation is below a threshold has a utility that is nonlinear in her belief. Anunrojwong, Iyer and Lingenbrink (2023) call such receivers risk-conscious and show that, for them, the standard revelation-principle reduction to action recommendations fails. Their first main result replaces it with a convex program over the joint distribution of state and action. This mission formalizes that result and the lemmas leading to it.

Setting

Let $\Omega$ be a finite set of states and $\Delta(\Omega) \subseteq \mathbb{R}^{\Omega}$ the simplex of beliefs, with the Euclidean topology. Sender and receiver share a prior $\mu^* \in \Delta(\Omega)$. The receiver chooses an action from a finite nonempty set $A$. Her utility is an arbitrary function $\rho : \Delta(\Omega) \times A \to \mathbb{R}$; the sender's utility is $v : \Omega \times A \to \mathbb{R}$.

For each action $a$, the beliefs at which $a$ is optimal for the receiver form the set

$$P_a = \{\mu \in \Delta(\Omega) : a \in \arg\max_{a' \in A} \rho(\mu, a')\}.$$

The paper assumes throughout (Assumption 1) that every $P_a$ is closed.

A signaling scheme consists of a measurable signal space $S$ and a probability measure $\pi$ on $\Omega \times S$ whose $\Omega$-marginal is $\mu^*$. After signal $s$ the receiver holds the posterior $\mu_s \in \Delta(\Omega)$ given by Bayes' rule, and plays an optimal strategy $a(\cdot)$, with $a(s) \in \arg\max_a \rho(\mu_s, a)$, that is $\mu_s \in P_{a(s)}$. The sender's persuasion problem (3) is to maximize $\mathbb{E}_\pi[v(\bar\omega, a(\bar s))]$ over signal spaces, schemes and optimal receiver strategies; when the receiver is indifferent, the sender picks the strategy she prefers.

A probability measure $\eta$ on $\Delta(\Omega)$ is Bayes-plausible if its mean is the prior: $\mathbb{E}_\eta[\bar s] = \mu^*$.

Formalization targets

Goal: Theorem 1

The sender's problem (3) can be optimized by solving the convex program

$$\max_{\{t_a : a \in A\}} \sum_{\omega \in \Omega} \sum_{a \in A} t_a(\omega)\, v(\omega,a) \quad \text{s.t.} \quad \sum_{a \in A} t_a(\omega) = \mu^*(\omega)\ (\omega \in \Omega), \qquad t_a \in \operatorname{Conv}(P_a \cup \{0\})\ (a \in A). \qquad (7)$$

It is formalized as an equality of sets: the values achievable in (3) are exactly the objective values of feasible points of (7). This says that every scheme yields a feasible point of (7) with the same value, and every feasible point is realized by a scheme. In particular the supremum of (3) equals the maximum of (7), and an optimal solution of (7) gives an optimal scheme.

Milestones

1. Lemma 1 (Aumann–Maschler, Kamenica–Gentzkow): schemes whose signals are beliefs and satisfy $\mu_s = s$ correspond to Bayes-plausible measures.
2. Lemma 5: the belief-recommendation problem (4) is equivalent to problem (14) over Bayes-plausible measures.
3. Lemma 2: a Bayes-plausible measure and an optimal strategy give action probabilities $b_a \in [0,1]$ and mean-posteriors $m_a \in \operatorname{Conv}(P_a)$ with $\sum_a b_a m_a = \mu^*$ and the same sender value; the converse also holds.

Further result: Theorem 2

Let $\Upsilon_a$ be the states at which $a$ is sender-optimal, assume these sets partition $\Omega$, and set $t^*_a = \mu^* \mathbb{1}_{\Upsilon_a}$. Then the sender can fully persuade the receiver (almost surely, the receiver takes a sender-optimal action) if and only if $t^*$ is feasible for (7), i.e. $t^*_a \in \operatorname{Conv}(P_a \cup \{0\})$ for all $a$.

Significance

The result. Problem (3) optimizes over arbitrary signal spaces and joint distributions, so it is not finite-dimensional. Program (7) has $|A|$ vector variables in $\mathbb{R}^{\Omega}$, each in a convex set that depends only on the receiver's utility. Its variable $t_a(\omega)$ is the joint probability of state $\omega$ and action $a$. The program gives the paper's bound on the number of signals needed (Proposition 1), its characterization of when persuasion helps (Proposition 2), the full-persuasion criterion (Theorem 2) and, after replacing $\operatorname{Conv}(P_a \cup \{0\})$ by a polytope, the linear program for binary persuasion (Theorem 3, the companion mission). For expected-utility receivers each $P_a$ is convex, and (7) reduces to the familiar obedience-constrained linear program.

Formalizing it. The results are proved in the paper; none is formalized. A formal development fixes what "can be optimized by solving" means as a set equality and handles general measurable signal spaces with posteriors defined only almost everywhere. It also exposes two places where the printed lemmas need correction (see the scope section).

Difficulty

The usual revelation-principle shortcut would merge all signals that lead to the same action. For a risk-conscious receiver this can change the response: averaging posteriors in $P_a$ can produce a belief outside $P_a$, since $P_a$ need not be convex. The central geometric difficulty is relating a distribution of posteriors supported on a closed, potentially nonconvex $P_a$ to a finite-dimensional variable in $\operatorname{Conv}(P_a \cup \{0\})$. The converse must preserve both Bayes plausibility and receiver optimality. With general signal spaces, the posterior is determined only almost everywhere, while the stated strategy condition applies at every signal.

Formalization scope

• Representation. $\Omega$ and $A$ are Fintypes, $A$ nonempty, and $\Omega$ carries a measurable space in which singletons are measurable. Beliefs are functions $\Omega \to \mathbb{R}$ in stdSimplex ℝ Ω, Belief Ω is the simplex as a subtype, $\operatorname{Conv}$ is convexHull ℝ, and $0$ is the zero function. $\rho$ is a function on $\mathbb{R}^{\Omega}$, used only on the simplex.
• Signal spaces in (3) range over all measurable types. A scheme is a probability measure on $\Omega \times S$ with $\pi(\{\omega\} \times S) = \mu^*(\omega)$.
• Posteriors are any version of Bayes' rule: simplex-valued for every signal, measurable, and satisfying $\pi(\{\omega\} \times B) = \int_B \mu_s(\omega)\,\pi_S(ds)$. Quotients $\pi(\omega,s)/\sum_{\omega'} \pi(\omega',s)$ with Lean's $x/0 = 0$ are not used. "$\mu_s = s$" (Lemmas 1 and 5) means the identity is such a version, an almost-sure statement; the paper's "for all $s$" in Lemma 1's converse is proved only almost surely.
• Strategies are measurable (each event $\{a(\bar s) = b\}$ is measurable) and optimal at every signal. The sender's value is not computed with a fixed tie-breaking rule, so sender-preferred selection is kept.
• Assumption 1 is a hypothesis of every statement that involves $\rho$.
• Corrections to Lemma 2. If some $P_a$ is empty, $\operatorname{Conv}(P_a)$ is empty and the printed forward direction fails, so $m_a$ is left free there; then $b_a = 0$ necessarily. The printed converse fails for pure strategies when two actions must share a posterior, so it is stated for optimal mixed strategies, which the paper allows on p. 11.
• Ruled out: quantifying (3) only over belief signals with $\mu_s = s$ would turn Theorem 1 into Lemmas 5 and 2 and drop the coalescence step. The goal therefore quantifies over arbitrary signal spaces. Stating only "the optimal values are equal" through a real supremum would also be weaker, and is not done.
• Infrastructure needed: means of probability measures on compact sets in $\mathbb{R}^n$ lying in the convex hull (Convex.integral_mem, compactness of convex hulls of compact sets), Carathéodory's theorem (convexHull_eq_union), finite discrete measures on $\Omega \times S$, and conditional densities with respect to the signal marginal. The Bayes-plausibility and splitting lemmas are reusable in any persuasion development. Proofs of the milestones, of the goal, and of Theorem 2 are all welcome.

Selected references

• J. Anunrojwong, K. Iyer, D. Lingenbrink, Persuading Risk-Conscious Agents: A Geometric Approach, arXiv:2208.03758v3, 2023; Operations Research, 2024. https://arxiv.org/abs/2208.03758v3
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• D. Bergemann, S. Morris, Bayes Correlated Equilibrium and the Comparison of Information Structures in Games, Theoretical Economics 11(2), 2016. https://doi.org/10.3982/TE1808

Why give data away

Firms that own data increasingly sell it as a product: market research panels, consulting reports, datasets for training demand models. A common commercial practice is to hand out a free sample of the data before quoting a price for the rest. Under standard Bayesian reasoning this practice looks self-defeating. Every free data point reduces the buyer's uncertainty, which reduces what the remaining data are worth to her. This is a holdup problem: once information is revealed, it cannot be sold.

Drakopoulos and Makhdoumi (Providing Data Samples for Free, SSRN 3611003; Management Science, 2022, doi:10.1287/mnsc.2022.4534) identify when free samples nevertheless raise the seller's revenue. The mechanism is disagreement about the prior. When the seller believes the buyer's initial estimate is biased, she expects the free data to move the buyer's belief toward states in which the buyer values the remaining data more. The paper calls this the persuasion benefit, and it can outweigh the holdup cost. This mission formalizes the paper's main theorem, Theorem 1(a), together with the lemmas its proof rests on.

The model

An unknown real parameter $\theta$ determines a buyer's payoff $u(a,\theta)$ from an action $a\in\mathbb R$. The Buyer holds the prior $\mathcal N(\theta_0,\sigma_0^2)$ with $\sigma_0^2>0$. The Seller believes $\theta_0$ is a biased estimate, with bias distributed as $\mathcal N(\mu_b,\sigma_b^2)$ and $\sigma_b^2\ge0$. Her prior is $\mathcal N(\theta_0+\mu_b,\sigma_s^2)$ with $\sigma_s^2=\sigma_0^2+\sigma_b^2$, and it is taken to be the correct one.

Data arrive continuously. The first $t\ge0$ samples are equivalent to the signal

$$Y_t=\theta t+\sigma B_t,$$

where $B$ is a standard Brownian motion independent of $\theta$ and $\sigma^2>0$ is the noise variance. Both parties agree on this law of the data given $\theta$ (they are concordant) and disagree only on the prior. The information after $t$ samples is $\mathcal F_t=\sigma(Y_s:s\le t)$.

The Buyer's posterior after $t$ samples is $\mathcal N(\theta_t,\sigma_t^2)$, with $\sigma_t^2=\sigma_0^2\sigma^2/(\sigma_0^2t+\sigma^2)$ and $\theta_t=(\sigma_t^2/\sigma_0^2)\theta_0+(\sigma_t^2/\sigma^2)Y_t$. The Seller's posterior $\mathcal N(\tilde\theta_t,\tilde\sigma_t^2)$ is given by the same formulas from her own prior. The Seller's estimate of the Buyer's error is $g_t=\tilde\theta_t-\theta_t$, and $g_0=\mu_b$.

With belief $\mathcal N(\theta,v)$, the Buyer's best expected utility is $U(\theta,v)=\max_a\mathbb E_{\mathcal N(\theta,v)}[u(a,\cdot)]$. Her Bayes risk

$$BR(\theta,v)=\mathbb E_{\mathcal N(\theta,v)}\big[\max_a u(a,\cdot)\big]-U(\theta,v)$$

is the value to her of learning $\theta$ exactly. Its second argument is a variance, and $BR_\theta$, $BR_{\theta\theta}$ and $BR_{\sigma^2}$ denote its partial derivatives.

A free-sample policy gives data for free up to a stopping amount $T$, a stopping time of $(\mathcal F_t)$, and then sells the remainder. Once the free samples stop, the best price for the remainder is $BR(\theta_T,\sigma_T^2)$ (Lemma 3). The Seller's expected revenue is therefore $\mathbb E^S_0[BR(\theta_T,\sigma_T^2)]$, computed under her prior. Selling in one round is $T=0$, with revenue $BR(\theta_0,\sigma_0^2)$.

Formalization targets

Goal: Theorem 1(a)

If the Seller-side drift of the Bayes risk is positive at the start,

$$\tfrac12 BR_{\theta\theta}(\theta_0,\sigma_0^2)-BR_{\sigma^2}(\theta_0,\sigma_0^2)+\frac{\mu_b}{\sigma_0^2}BR_\theta(\theta_0,\sigma_0^2)>0, \tag{4}$$

then some free-sample policy $T$ satisfies

$$\mathbb E^S_0\big[BR(\theta_T,\sigma_T^2)\big]>BR(\theta_0,\sigma_0^2).$$

The goal has no constants. It asserts only that the optimal free-sample policy strictly beats every one-round policy.

Milestones

• Proposition 1 (p. 13): the posteriors given the whole data path are the Gaussians above.
• Lemma 1(i)–(iii) (p. 14): the posterior variance decreases at rate $\sigma_t^4/\sigma^2$. The Buyer's estimate has drift $0$ for the Buyer and $g_t\sigma_t^2/\sigma^2$ for the Seller. Its squared increment is $\sigma_t^4/\sigma^2\,dt+O(dt^{3/2})$.
• Lemma 3 (p. 16): the Buyer pays at most $BR$ for any partial release, and exactly $BR$ for full release.
• Lemma 4(b) (p. 17): from the Seller's perspective, $\mathbb E^S[BR(\theta_h,\sigma_h^2)]$ has initial slope $\big(\tfrac12BR_{\theta\theta}-BR_{\sigma^2}+\tfrac{\mu_b}{\sigma_0^2}BR_\theta\big)\sigma_0^4/\sigma^2$.
• Lemma 4(a) (p. 17): from the Buyer's perspective, the same with $\mu_b$ replaced by $0$.
• Theorem 1(b) (p. 18): if the Seller-side drift is non-positive for every posterior mean, misspecification, and positive variance, then no free-sample policy beats selling in one round.

Significance

Theorem 1 splits the drift of the Bayes risk from the Seller's viewpoint into a holdup cost, $\tfrac12BR_{\theta\theta}-BR_{\sigma^2}$, which is the drift the Buyer herself expects, and a persuasion benefit, $(g_t/\sigma_t^2)BR_\theta$. Part (a) turns the sign of this drift at the start into a revenue comparison. In the paper's pricing example (unknown demand elasticity, $BR(\theta,v)=\tfrac14e^{-\theta}(e^{v/2}-e^{-v/2})$), condition (4) reduces to $\mu_b<\sigma_0^2/(1-e^{\sigma_0^2})$: a sufficiently biased Buyer should be given free data. In the estimation example ($BR=\sigma_t^2$) part (b) applies and one-round selling is optimal. The theorem is the basis of the paper's later results on myopic stopping rules and on the comparison with dynamic pricing.

The theorem is proved in the paper, in $dt$-notation and through Itô's lemma and the optional stopping theorem. It has not been machine-checked. A formal proof requires Gaussian conjugacy with respect to a Brownian filtration, moment computations for the posterior mean, an Itô-type expansion for a $C^2$ function of the belief, and control of the integrability of the stopped Bayes risk. Each of these is reusable for other continuous-time Bayesian learning models.

Difficulty

The informal argument reads off Lemma 4 that $BR(\theta_t,\sigma_t^2)$ is a Seller-submartingale near the start, and then stops it. The $dt$-identities of Lemmas 1 and 4 are statements about conditional expectations at every time. Made rigorous, they require integrability of the Bayes risk and its derivatives along the belief path, and an exchange of differentiation and expectation. Neither is given by the paper's hypotheses on $u$. The Gaussian conjugacy itself must also be established for conditioning on the whole path $(Y_s)_{s\le t}$, not only on $Y_t$.

Formalization scope

All objects are defined in one file, FreeSamples.Revenue.Setting, on top of Mathlib's gaussianReal, IsBrownianReal, Filtration.natural and IsStoppingTime. Committed conventions:

• Variances are real numbers, and $\mathcal N(m,v)$ is gaussianReal m v.toNNReal. $BR$ and $U$ take the variance, not the standard deviation, as their second argument.
• A model with prior $\mathcal N(m,v)$ is a probability space carrying measurable $\theta\sim\mathcal N(m,v)$ and a Brownian motion $B$ independent of $\theta$. The Seller's and the Buyer's measures are the two instances, which makes concordance hold by construction. Every revenue is an expectation under the Seller's measure.
• The filtration is the natural filtration of $Y$ without augmentation. Free-sample policies are bounded stopping times. The paper requires only measurability of $T$, but its own construction is bounded by a large constant $M$.
• Standing hypotheses on $u$, all disclosed pins: the maxima in $U$ and $BR$ exist and are attained, with all expectations integrable (HasMax); Assumption 1 is read as $U,BR\in C^2(\mathbb R\times(0,\infty))$; and $BR$ and its partial derivatives grow at most like $Ce^{c|\theta|}$ for variances in $(0,\sigma_0^2]$.
• The $dt$-statements of Lemmas 1 and 4 are posed as one-sided derivatives at time $0$ of plain expectations, for arbitrary parameters. The time-$t$ versions follow by restarting from the posterior state and are not posed.
• Lemma 4's printed factor $\sigma_t^4/\sigma_0^2$ is formalized as $\sigma_t^4/\sigma^2$, as Lemma 1 gives. Condition (5) of Theorem 1(b) keeps the page's universal quantifiers over the posterior mean, misspecification and positive variance. Quantification over all $g_t$ forces $BR_\theta\equiv0$; the paper's application on p. 33 checks only the realized $g_t$, so it does not establish the printed condition for that example.

Trivializing formalizations are ruled out. Every revenue in a conclusion is asserted integrable, so a junk-zero integral cannot satisfy it. The maxima in $U$ and $BR$ are assumed attained, so no real supremum takes its junk value. The goal is stated for the Gaussian–Brownian model and its posterior map, not for an arbitrary process with a postulated drift. Its conclusion exhibits a policy instead of comparing a supremum over policies.

Not posed: the stochastic differential equation of Lemma 1, Lemma 2, Proposition 2 (its free boundary is part of the hypothesis), Corollaries 1–3, and Appendix B. Contributions are welcome on the conjugacy computation (Proposition 1), on the Gaussian moment estimates (Lemma 1), and on a reusable Itô-type expansion of $h\mapsto\mathbb E[F(m_h,v_h)]$ for $C^2$ functions of exponential growth.

Selected references

• K. Drakopoulos and A. Makhdoumi, Providing Data Samples for Free, SSRN 3611003; Management Science, 2022. https://ssrn.com/abstract=3611003, https://doi.org/10.1287/mnsc.2022.4534
• S. Morris, Trade with Heterogeneous Prior Beliefs and Asymmetric Information, Econometrica 62(6), 1994. https://doi.org/10.2307/2951755
• R. J. Aumann, Agreeing to Disagree, Annals of Statistics 4(6), 1976. https://doi.org/10.1214/aos/1176343654
• J. M. Steele, Stochastic Calculus and Financial Applications, Springer, 2001. https://doi.org/10.1007/978-1-4684-9305-4

Motivation

Model-based reinforcement learning algorithms for Markov decision processes estimate each transition distribution $P_{s,a}$ from the transitions they have observed out of the state–action pair $(s,a)$. Their regret analyses then need to know how far the empirical distribution $\hat p$ can be from the true one $p$. The standard tool is an $\ell_1$ bound on $\hat p-p$, as in UCRL2 (Jaksch, Ortner and Auer, 2010), which costs a factor of order $\sqrt S$ in the number of states $S$. What the analysis actually uses, however, is the deviation along one direction: the projection $(\hat p-p)^Th$ onto a bias (or value) vector $h$ whose entries differ by at most the MDP's diameter $D$.

S. Agrawal and R. Jia (arXiv:1705.07041v3, published in Mathematics of Operations Research, 2023, as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds) prove a worst-case regret bound of order $\tilde O(D\sqrt{SAT})$ for an optimistic variant of posterior sampling. One ingredient of that analysis is their Proposition 5.2: a Bernstein-type bound on $(\hat p-p)^Th$ whose leading term is governed by a variance of $h$ under $p$, written in stick-breaking form. This mission formalizes that proposition and the steps of its proof.

Setting

Fix a number of states $S$ and order them $1,\dots,S$. A probability vector $p\in\Delta^S$ has $p_i\ge0$ and $\sum_ip_i=1$. A multinoulli trial with parameter $p$ is a random state $X$ with $\mathbb P(X=i)=p_i$. Draw $n$ independent trials $X_1,\dots,X_n$ and let

$$\hat p_i=\frac{\#\{t: X_t=i\}}{n}$$

be the empirical probability vector, the average of the one-hot outcomes. For $p$ and a vector $h\in\mathbb R^S$ define the stick-breaking quantities

$$\gamma_i=\frac{p_i(p_{i+1}+\cdots+p_S)}{p_i+\cdots+p_S},\qquad H_{i+1}=\frac{1}{\sum_{j=i+1}^Sp_j}\sum_{j=i+1}^Sh_jp_j,\qquad c_i=h_i-H_{i+1}.$$

Thus $H_{i+1}$ is the mean of $h$ under $p$ conditioned on the states after $i$, and $c_i$ compares $h_i$ with it. The sum $\sum_{i<S}\gamma_ic_i^2$ equals the variance of $h(X)$ for $X\sim p$. In Lean these objects are gammaCoef p i, Hnext p h i, cCoef p h i, phat ω i, the law of one trial is cat p and the law of $n$ trials is trialsLaw n p, all in the namespace OptimisticPSRL.Concentration.

Formalization targets

Goal: Proposition 5.2 (p. 9)

Let $h\in\mathbb R^S$ satisfy $|h_i-h_{i'}|\le D$ for all $i,i'$, let $n\ge96$ and $\rho\in(0,1)$. Then, with probability at least $1-\rho$,

$$\big|(\hat p-p)^Th\big|\le2\sqrt{\log(n/\rho)\sum_{i<S}\frac{\gamma_ic_i^2}{n}}+3D\,\frac{\log(2/\rho)}{n}.$$

Milestones

1. Fact 1 (p. 17), a deterministic identity: for probability vectors $\tilde p,\bar p$ with stick-breaking ratios $\tilde y_i=\tilde p_i/(\tilde p_i+\cdots+\tilde p_S)$ and $\bar y_i$,

$$(\tilde p-\bar p)^Th=\sum_i(\tilde y_i-\bar y_i)(h_i-\tilde H_{i+1})(\bar p_i+\cdots+\bar p_S)=\sum_i(\tilde y_i-\bar y_i)(h_i-\bar H_{i+1})(\tilde p_i+\cdots+\tilde p_S).$$

2. The projection as a sum of martingale differences (proof, p. 21): with $Z_{t,i}=c_i\mathbb 1(X_t=i)-c_i\frac{p_i}{p_i+\cdots+p_S}\mathbb 1(X_t\ge i)$ and $Z_t=\sum_iZ_{t,i}$,

$$\frac1n\sum_{t=1}^nZ_t=(\hat p-p)^Th,$$

together with the two intermediate expressions of the page. 3. Uncorrelated coordinates (proof, p. 21): $\mathbb E[Z_{t,i}Z_{t,j}]=0$ for $i\ne j$. 4. The predictable variance (proof, p. 21): $\sum_{t=1}^n\mathbb E[Z_t^2]=\sum_ic_i^2\,n\,\gamma_i$. 5. Corollary B.1 (p. 26), Bernstein's inequality for bounded martingale differences with random predictable variance $V_n$: for $n\ge96$, $\delta\in(0,1)$, with probability greater than $1-\delta$,

$$|M_n|\le2\sqrt{V_n\ln(n/\delta)}+3K\ln(n/\delta).$$

Significance

The result. Proposition 5.2 is the concentration half of the optimism step of the paper (Lemma 5.3): combined with an anti-concentration bound for Dirichlet samples along the same direction (Proposition 5.1), it shows that some posterior sample is optimistic along $h$ with constant probability. Because the bound is stated along a single direction and is weighted by the variance of $h$ rather than by $D$ alone, it avoids the $\sqrt S$ loss that an $\ell_1$ bound would incur, which is part of how the paper's regret bound improves on UCRL2's $\tilde O(DS\sqrt{AT})$. The stick-breaking form of the variance is what lets the same quantity appear on both sides of the optimism argument, in the Dirichlet bound and in the empirical bound.

Formalizing it. The proposition and its proof steps are proved on paper; none of them has a machine-checked proof. The regret theorem of the paper (Theorem 1) is not posed: its constants are hidden in $O(\cdot)$ and its algorithm's parameters are given as $\Theta(\cdot)$. Proposition 5.2, by contrast, is fully explicit. Corollary B.1 is a reusable martingale inequality with explicit constants. The predictable-variance identity and Fact 1 are exact identities about stick-breaking coordinates that recur in analyses of Dirichlet and categorical models.

Difficulty

Two steps resist the obvious approach. First, the statement carries the variance in stick-breaking form, not as $\mathrm{Var}_p(h)$; linking the two needs the decomposition of Fact 1 and the identity for the predictable variance, which are exact algebraic identities whose bookkeeping of tails and empty tails is error-prone. Second, the paper's own route goes through Corollary B.1, a martingale Bernstein inequality with a random variance, which rests on a peeling argument over a grid of variance levels (Seldin et al., 2012); Mathlib has neither this inequality nor a Bernstein inequality with explicit constants for bounded variables.

A known subtlety: the paper's proof, through Corollary B.1, yields the second term $3D\log(n/\rho)/n$, while the statement prints the smaller $3D\log(2/\rho)/n$. The printed statement is still true for $n$ iid trials (the classical Bernstein inequality gives a bound below it), so the goal is posed as printed. The paper's own proof therefore does not establish the printed constant.

Formalization scope

• States are Fin S with its natural order, 0-based; the paper's range $i<S$ is every state but the last (belowLast S). Fact 1 holds for every ordering; the natural order covers this since states are labels.
• Probability vectors are p : Fin S → ℝ with IsProbVec p (nonnegative, summing to one). Zero entries are allowed. A ratio whose denominator is zero evaluates to $0$ (Lean's convention), which gives the values the identities need; no positivity of $p$ is assumed.
• One trial has law cat p $=\sum_ip_i\delta_i$; $n$ trials have the product law trialsLaw n p $=$ Measure.pi. The empirical vector phat ω is computed from the sample ω : Fin n → Fin S. "With probability $1-\rho$" is ENNReal.ofReal (1 - ρ) ≤ trialsLaw n p {good event}; Corollary B.1's "greater than $1-\delta$" is strict. $\log$ is Real.log.
• The proof displays (milestones 2–4) are stated in the iid reading of the proposition: the paper writes them for transitions of an MDP out of a fixed $(s,a)$, with an indicator $\mathbb 1(s_{t-1}=s,a_{t-1}=a)$ and a random count $\tau$; here the indicator is one and $\tau=n$, and the conditional expectations are expectations under one draw of law $p$. Milestone 2 assumes every drawn state has positive probability (true almost surely), which the page's intermediate sum over $i\le S-1$ needs.
• Corollary B.1 is posed for a general filtered probability space, with $Z_i$ $\mathcal F_i$-measurable, $|Z_i|\le K$ almost surely and $\mathbb E[Z_i\mid\mathcal F_{i-1}]=0$.

The goal cannot be satisfied by a degenerate reading: $\hat p$ is built from the sample, the measure is the $n$-fold product of the categorical law $p$, the event is the good event itself (not a complement bound), and the variance term is not identically zero (for $S=2$, $p=(\tfrac12,\tfrac12)$ it equals $(h_1-h_2)^2/4$).

Needed infrastructure: finite-sum manipulations over tails of Fin S; a Bernstein or Freedman inequality with explicit constants (for iid bounded variables for the goal, for martingale differences for Corollary B.1). Contributions of either inequality are reusable well beyond this mission and are welcome, as are alternative proofs of the goal that bypass Corollary B.1.

Selected references

• S. Agrawal and R. Jia, Posterior sampling for reinforcement learning: worst-case regret bounds, arXiv:1705.07041v3, 2020; published as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1705.07041
• T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/jaksch10a.html
• Y. Seldin, F. Laviolette, N. Cesa-Bianchi, J. Shawe-Taylor and P. Auer, PAC-Bayesian inequalities for martingales, IEEE Transactions on Information Theory 58(12), 2012. https://doi.org/10.1109/TIT.2012.2211334

Motivation

Cutting plane methods minimize a convex function, or find a point in a convex set, using only a separation oracle: a routine that, given a query point, either certifies it is good or returns a halfspace containing the target. Lee, Sidford and Wong (arXiv:1508.04874, FOCS 2015) gave a cutting plane method for a convex set in $\mathbb R^n$ inside a box of radius $R$ that uses an expected $O(n\log(nR/\epsilon))$ oracle calls and $O(n^3\log^{O(1)}(nR/\epsilon))$ additional time, improving on the $O(n^{\omega+1}\log(nR/\epsilon))$ additional time of Vaidya's method from over 25 years earlier, and derived from it faster algorithms for submodular function minimization, matroid intersection and submodular flow.

The speed-up depends on not recomputing the leverage scores of the current constraint matrix from scratch at every step. The algorithm maintains approximations and refreshes a few of them per step. Section 7.2 of the paper isolates the bookkeeping question this raises as a two-player game, the stochastic chasing $\vec 0$ game, and shows that a simple greedy strategy keeps the accumulated error small. The game is self-contained and has nothing to do with convexity: it is a statement about a random walk in $\mathbb R^m$ that is partially reset at every step.

Setting

Fix a dimension $m\ge1$ and constants $c>0$, $R>0$. For $\vec v\in\mathbb R^m$, $\|\vec v\|_\infty=\max_i|v_i|$ and $\|\vec v\|_2=(\sum_iv_i^2)^{1/2}$.

A point starts at $\vec x^{(1)}=\vec 0$. Each round $k=1,2,\dots$ runs as follows (Algorithm 4).

1. A stochastic adversary chooses a probability distribution $\mathcal D^{(k)}$ on $\mathbb R^m$ with mean $\vec 0$ and $\|\vec\Delta\|_2\le c$ for every $\vec\Delta$ in its support.
2. The adversary chooses an observation $\vec y^{(k)}$ with $\|\vec y^{(k)}-\vec x^{(k)}\|_\infty\le R$.
3. The player chooses a coordinate $i^{(k)}$, knowing only $\vec y^{(k)}$: neither $\vec x^{(k)}$, nor $\mathcal D^{(k)}$, nor the step.
4. A step $\vec\Delta^{(k)}$ is drawn from $\mathcal D^{(k)}$ and the point moves to

$$x^{(k+1)}_{i^{(k)}}=0,\qquad x^{(k+1)}_j=x^{(k)}_j+\Delta^{(k)}_j\quad(j\ne i^{(k)}).$$

The adversary may use everything that has happened so far to make its choices. The player wants to keep $\vec x^{(k)}$ near $\vec 0$ in $\|\cdot\|_\infty$; the adversary wants to push it away. The largest-coordinate strategy is $i^{(k)}=\operatorname{argmax}_i|y^{(k)}_i|$: reset the coordinate that looks largest.

Formalization targets

Goal: Theorem 34

If the player uses the largest-coordinate strategy, then for every $p\in(0,1]$, with probability at least $1-p$,

$$\|\vec x^{(k)}\|_\infty\le2(c+R)\log\big(4mk^2/p\big)\qquad\text{for all }k\ge1.$$

The bound holds simultaneously for all rounds, against every adaptive adversary, and grows only logarithmically in $k$, in $m$ and in $1/p$.

Milestones

The milestones are the steps that the paper's proof of Theorem 34 (pp. 43–44) displays:

1. the exponential inequality $e^x\le1+x+\tfrac{x^2}{2}e^{|x|}$ and its consequence $e^{\alpha x+\alpha\delta}\le e^{\alpha x}+\alpha\delta e^{\alpha x}+\tfrac12\alpha^2\delta^2e^{\alpha x+|\alpha|c}$ for $|\delta|\le c$;
2. the one-step drift bound for the potential $\Phi(\vec x)=\sum_ie^{\alpha x_i}+\sum_ie^{-\alpha x_i}$:

$$\mathbb E_{\vec\Delta\sim\mathcal D}\,\Phi(\vec x+\vec\Delta)\le\Phi(\vec x)+\alpha^2e^{\alpha c}c^2\eta,\qquad\eta=\max\big(\max_ie^{\alpha x_i},\max_ie^{-\alpha x_i}\big);$$

3. the choice $\alpha=1/(2(c+R))$, for which $e^{2\alpha(c+R)}(\alpha(c+R))^2\le1$ and $\alpha^2e^{\alpha c}c^2\le e^{-\alpha(R+c)}$;
4. the union-bound arithmetic $1-\sum_{k\ge1}2m/\lambda_k=1-\sum_{k\ge1}p/(2k^2)\ge1-p$ for $\lambda_k=4mk^2/p$.

Significance

Within the paper, Theorem 34 is what lets the cutting plane method keep its leverage-score estimates within a bounded multiplicative error while refreshing only one estimate per step; this is one of the ingredients behind the $O(n^3\log^{O(1)}(nR/\epsilon))$ additional time. The game reappears whenever an algorithm tracks many slowly drifting quantities with noisy observations and can afford to recompute only a few of them exactly per step, which makes the statement useful beyond this paper.

None of the statements in this mission has a machine-checked proof. The theorem is published with a proof. The mission asks for a formal proof of the statement exactly as published, with the constant $4$ inside the logarithm. A formal proof of the milestones alone would already give a reusable exponential-potential toolkit for adaptive random processes in $\mathbb R^m$.

Difficulty

The point process is not a martingale: the player's resets depend on a noisy observation, the adversary is adaptive, and the reset can hit a coordinate that is up to $2R$ smaller in absolute value than the largest one. Per-coordinate tail bounds do not suffice, because the adversary may concentrate its moves on whichever coordinates the player is not resetting. A bound that holds for all $k$ at once, with only logarithmic dependence on $k$, has to control all coordinates jointly. Establishing such joint control, with the specific constant $4$ inside the logarithm, against the most adversarial interaction between the observation error $R$ and the step size $c$, is where the work lies.

Formalization scope

• Probability model. The randomness is a probability space $(\Omega,\mu)$ with a filtration $(\mathcal F_k)_{k\ge0}$. The adversary's adaptive choice of $\mathcal D^{(k)}$ is modelled by the conditional law of the step: each coordinate of the step has conditional mean $0$ given the past, the step is measurable with respect to the next $\sigma$-algebra, and $\sum_i\Delta_i^2\le c^2$ holds everywhere. The observation $\vec y^{(k)}$ is measurable with respect to the current $\sigma$-algebra, so it is fixed before the step is drawn, and $\|\vec y^{(k)}-\vec x^{(k)}\|_\infty\le R$ holds on the actual trajectory.
• Indexing. Coordinates are Fin m (0-based), with $m\ge1$. Lean round $k\in\mathbb N$ is the paper's round $k+1$, so the goal's bound reads $\log(4m(k+1)^2/p)$; at Lean round $0$ the point is $\vec 0$.
• Norms. $\|\cdot\|_\infty$ is Lean's sup norm on Fin m → ℝ. The step bound $\|\vec\Delta\|_2\le c$ is written as $\sum_i\Delta_i^2\le c^2$, never as a sup-norm bound. The paper's prose once writes $\|\vec\Delta\|_2^2\le c$; Algorithm 4 and the proof use $\|\vec\Delta\|_2\le c$, which is what is formalized.
• Tie rule. $\operatorname{argmax}_i|y_i|$ breaks ties by the least index; the paper's theorem is claimed for any tie rule.
• Constants. $c>0$, $R>0$ (Algorithm 4), $0<p\le1$, natural logarithm. The drift milestone adds $\alpha\ge0$.
• Not trivial by construction. The hypotheses are satisfiable by genuinely random adversaries (a fair-coin step of size $c$ is one), and the conclusion is a probability lower bound on an event, not a statement that holds vacuously; a formalization in which the observation could depend on the step, or in which the step bound were a sup-norm bound, would not be the paper's theorem.
• Out of scope. Running time, the leverage-score application (Section 7.1, Theorem 31) and the rest of the cutting plane method.
• Infrastructure. Conditional expectation with respect to a filtration, Markov's inequality and countable union bounds are in Mathlib. Supermartingale lemmas for nonnegative adapted processes, and the passage from a per-step drift inequality to a bound on the expected potential, are reusable well beyond this mission. Proofs of individual milestones are welcome independently of the goal.

Selected references

• Y. T. Lee, A. Sidford, S. C. Wong, A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization, FOCS 2015; arXiv:1508.04874v2, 2015. https://arxiv.org/abs/1508.04874
• P. M. Vaidya, A new algorithm for minimizing convex functions over convex sets, FOCS 1989; Mathematical Programming 73 (1996) 291–341. https://doi.org/10.1007/BF02592216

Motivation

Mobile retail stalls (self-driving or driver-operated vending vehicles that move to customers who order through a phone app) are studied by Cao and Qi in Stall Economy: The Value of Mobility in Retail on Wheels (Operations Research, 2022; the mission cites the authors' SSRN manuscript 3711896). A retailer partitions a city into service zones, one stall per zone, and must decide how densely to deploy stalls. That decision is made by continuous approximation: each zone is modelled as a small queueing system whose service time includes the stall's travel to the next customer. The mean and variance of that travel distance enter the Pollaczek–Khinchine waiting-time formula of an M/G/1 queue (the paper's equations (1a)–(2), p. 18), so closed forms for them are the input of the paper's whole deployment and pricing analysis (§4).

The paper considers two on-demand modes. In the door-to-door mode the stall drives to each customer's doorstep. In the within-radius mode each customer walks up to a distance $r$ toward the stall, and the stall only moves until the two are $r$ apart. This mission formalizes the travel-distance moments of both modes: Proposition 1 (door-to-door, p. 11) and Proposition 3 (within-radius, p. 18), whose proofs are in the paper's Appendix B (pp. 44–45 and 49–51).

Setting

All distances are Manhattan ($\ell_1$) distances (p. 9): $|A-B| = |a_1-b_1| + |a_2-b_2|$. A service zone is a square rotated by $45^\circ$, a diamond, of Euclidean edge length $R>0$; the paper sets $R = R(\rho) = 1/\sqrt\rho$ for a stall density $\rho$ (p. 11). In Manhattan coordinates centred at the zone's centre,

$$\mathcal Z_R = \{(x,y) : |x|+|y| \le R/\sqrt2\},$$

which has area $R^2$. Customers arrive uniformly on $\mathcal Z_R$.

Fix a walking radius $0\le r\le R/\sqrt2$. The inner diamond $\mathcal I_{R,r} = \{|x|+|y|\le R/\sqrt2-r\}$ lies $r$ inward from the boundary and has edge length $R-\sqrt2 r$. The paper's model for the stall's position when a new customer arrives (proof of Proposition 3, p. 49) is: the stall $A$ is uniform on $\mathcal I_{R,r}$, the customer $B$ is uniform on $\mathcal Z_R$, and the two are independent. The repositioning trip length is

$$L_r = \max\{|A-B| - r,\ 0\},$$

and $L_0' = |A-B|$ denotes the untruncated distance. In the door-to-door case $r=0$, both points are uniform on the zone and $L_0 = |A-B|$. The variance is $\operatorname{Var}(L_r) = \mathbb E[L_r^2]-\mathbb E[L_r]^2$.

The uniform law of the stall is the paper's Theorem 1 (the subject of the companion mission I), read in a continuum limit that the paper states informally (p. 17). This mission takes the uniform law as its model and does not depend on that limit.

Formalization targets

Goal: Proposition 3 (p. 18)

For all $R>0$ and $0\le r\le R/\sqrt2$,

$$\mathbb E[L_r] = \frac{7\sqrt2R^3-22R^2r+2\sqrt2Rr^2+12r^3}{15R^2},$$ $$\operatorname{Var}(L_r) = \frac{22R^6-22\sqrt2R^5r-140\sqrt2R^3r^3+400R^2r^4-48\sqrt2Rr^5-144r^6}{225R^4},$$

and both are non-decreasing in $R$ (on $\{R : r\le R/\sqrt2\}$) and non-increasing in $r$ (on $[0,R/\sqrt2]$).

Milestones, in the order of the proof

1. Proposition 1 (p. 11): $\mathbb E[L_0] = 7\sqrt2R/15$ and $\operatorname{Var}(L_0) = 22R^2/225$.
2. $\mathbb E[L_0'] = \tfrac{7\sqrt2R}{15}-\tfrac{7r}{15}+\tfrac{2\sqrt2r^2}{15R}+\tfrac{2r^3}{15R^2}$ (p. 49).
3. $\mathbb P(L_0'\le r) = 2r^2/R^2$ and $\mathbb E[L_0'\,\mathbf 1\{L_0'\le r\}] = \tfrac23r\cdot 2r^2/R^2$ (p. 50).
4. $\mathbb E[X^2] = (R^2-\sqrt2Rr+r^2)/6$ for the horizontal component $X$ of $|A-B|$ (p. 50).
5. $\mathbb E[(L_0')^2] = (8R^4-8\sqrt2R^3r+7R^2r^2+r^4)/(15R^2)$ (p. 51).
6. $\mathbb E[(L_0')^2\,\mathbf 1\{L_0'\le r\}] = \tfrac12r^2\cdot 2r^2/R^2$ (p. 51).
7. Proposition 3(I) and 8. Proposition 3(II) on their own.

A supporting theorem, $\mathbb E[XY] = (3R^4-3\sqrt2R^3r+2R^2r^2+r^4)/(30R^2)$ (p. 50), is posed as well.

Significance

The result. With Proposition 3 the service time of the within-radius mode has explicit first and second moments, so the M/G/1 waiting time, the stall's daily travel, and the profit density of §4 are explicit functions of $(\rho, r)$. Part (III) is the qualitative content the paper calls the first effect of avoiding the "last 100 meters": a longer customer walk shortens the stall's repositioning, and a larger zone lengthens it. Proposition 1 is the $r=0$ benchmark against which that saving is measured.

Formalizing it. The results are proved in the paper by direct integration; none is machine-checked. The proofs split the domain into several regions by the signs of coordinate differences and assert the values of the resulting polynomial integrals "by calculation". A formal proof checks every one of those integrals, the use of conditional expectations given the event $\{L_0'\le r\}$, and the derivative signs behind part (III), which the paper states without verification on the whole range. The intermediate moments are useful on their own for other models with uniform demand on diamonds under the Manhattan metric.

Difficulty

The obvious route rotates the diamond by $45^\circ$, where the $\ell_1$ distance becomes an $\ell_\infty$ distance and the zone a square, and then integrates. For $r=0$ this works cleanly. For $r>0$ the stall's square is smaller than the customer's, and $\max\{\cdot\}$ of two coordinate differences over two squares of different sizes splits into many polynomial pieces. The paper instead stays in the original coordinates and splits into six regions for $\mathbb E[XY]$. Either way, the truncation at $r$ is the delicate step: it requires that the whole $\ell_1$ ball of radius $r$ around the stall lies in the zone, which is exactly why the stall is confined to the inner diamond. Part (III) is not a consequence of (I) and (II) by inspection: the derivative in $R$ of the mean vanishes at the boundary $r = R/\sqrt2$, so the sign argument must be done on the closed range.

Formalization scope

Points are elements of ℝ × ℝ with Lebesgue measure. The definition StallEconomy.TripLength.Setting provides zone R, innerZone R r, the scale factor shrink R r = 1 − √2 r / R, the Manhattan distance l1, the trip length Lr r, the expectation E R r F, meanL R r and varL R r. The stall's uniform law is realised as $A = s\,U$ with $s = 1-\sqrt2r/R \in [0,1]$ and $U$ uniform on $\mathcal Z_R$, which is the uniform law on $\mathcal I_{R,r}$; it covers the endpoint $r=R/\sqrt2$, where the inner diamond is a single point, without dividing by $(R-\sqrt2r)^2$. Thus

$$\mathbb E[F(A,B)] = R^{-4}\int_{\mathcal Z_R}\int_{\mathcal Z_R} F(s\,u, b)\,db\,du.$$

Standing conventions and deviations from the page:

• every statement assumes $R>0$, and the within-radius statements $0\le r\le R/\sqrt2$, the paper's range;
• $R$ is the edge length itself, not $1/\sqrt\rho$;
• the conditional expectations given $\{L_0'\le r\}$ of pp. 50–51 are stated as truncated expectations $\mathbb E[\,\cdot\,\mathbf 1\{L_0'\le r\}]$, since the conditioning event has probability $0$ at $r=0$;
• the printed slips "$\mathbb P(L_0>r)$" (p. 50, $L_0'$ meant) and the conditioning event "$L_0'^2\le r$" (p. 51, $L_0'\le r$ meant) are corrected;
• "increasing/decreasing" in part (III) is weak monotonicity.

Formalizations that would trivialize the goal are ruled out: meanL and varL are integrals, not the closed forms; part (III) is stated about those integrals, not about the polynomials; and nothing is restricted to $r=0$ or to a fixed $R$.

A complete development needs iterated set integrals of piecewise polynomials over diamonds in ℝ × ℝ (Fubini on zone R, the change of variables $u\mapsto su$), and elementary calculus for part (III). Contributions of any of the moments, of a reusable lemma computing integrals of polynomials over diamonds, and of the monotonicity of the closed forms are all welcome. Proposition 2 of the paper, which is false as printed, is not claimed here.

Selected references

• J. Cao and W. Qi, Stall Economy: The Value of Mobility in Retail on Wheels, Operations Research, 2022 (articles in advance). https://doi.org/10.1287/opre.2022.2404 ; manuscript: SSRN 3711896, https://ssrn.com/abstract=3711896
• G. F. Newell, Dispatching policies for a transportation route, Transportation Science 5(1) 91–105, 1971 (origin of continuous approximation). https://doi.org/10.1287/trsc.5.1.91

Motivation

A permissioned blockchain is a shared ledger to which only approved participants may write. In supply chains it is proposed as a way to make product information (origin, quality, which supplier fulfilled an order) verifiable to buyers. Iyengar, Saleh, Sethuraman and Wang (SSRN 3602376; Management Science 2023, doi:10.1287/mnsc.2022.4532) ask who gains from such adoption and who pays for it.

Their first main result (Proposition 4.8, the subject of the companion mission I) identifies an adoption failure: when products differ strongly in how well they match consumers' tastes, full adoption raises total welfare, yet no manufacturer adopts, because price competition leaves manufacturers no profit with which to recover the adoption cost while the information gain accrues to consumers. Their second main result, Proposition 4.9, the goal of this mission, shows that a simple self-financing mechanism removes the failure: charge consumers a fee for access to the blockchain's information and pass the proceeds to the manufacturers.

Setting

There are $4m$ manufacturers, $m\ge 2$. Manufacturer $i$ has a horizontal type $q_i\in\{A,B\}$ and a vertical type $\xi_i\in\{h,l\}$; each of the four type classes has exactly $m$ members. Joining the blockchain costs manufacturer $i$ an amount $\chi_i>0$; $a_i\in\{0,1\}$ records the decision. A unit mass of consumers values a matching product at $H$ and a mismatched one at $L$, with $0\le L<H$, plus a vendor quality $h>l\ge 0$; the high-quality vendor has marginal cost $\gamma>0$. Each consumer $k$ also has an outside option $\phi_k$, drawn from a continuous distribution $G$ supported on $[0,\infty)$. The parameter of interest is the horizontal differentiation $\Delta=H-L$; $L$ is held fixed and $H=L+\Delta$.

Under full adoption, a consumer who has access to the blockchain's information finds a best product utility $\Delta+L+h-\gamma$; without access, only $\Delta/2+L+h-\gamma$. A system of transfers $(\kappa,\{\tau_i\}_{i\in M})$ charges each consumer who wants access a fee $\kappa$ and pays manufacturer $i$ an amount $\tau_i\ge 0$. A consumer pays ($b_k=1$) when

$$\max\{\Delta+L+h-\gamma,\phi_k\}-\kappa\ \ge\ \max\Big\{\tfrac{\Delta}{2}+L+h-\gamma,\phi_k\Big\},$$

and $\mu_\kappa$ denotes the mass of paying consumers. The system is self-financing if

$$\kappa\cdot\mu_\kappa=\sum_{i\in M}\tau_i. \tag{14}$$

Manufacturer $i$ earns $\Pi(a_i,a_{-i})-\chi_i a_i+\tau_i a_i$ (15), where the gross profit $\Pi$ is zero because of price competition. The system overcomes adoption failures if full adoption ($a_i=1$ for all $i$) is an equilibrium of this game.

The proof of Proposition 4.9 uses the fee $\kappa=\sum_i\chi_i/G(\phi)$ and the gain from access

$$h(\phi_k;\phi)=\max\{\Delta+L+h-\gamma,\phi_k\}-\frac{\sum_{i\in M}\chi_i}{G(\phi)}-\max\Big\{\frac{\Delta}{2}+L+h-\gamma,\phi_k\Big\}.$$

Formalization targets

Goal: Proposition 4.9 (p. 21)

$$\exists\,\Delta_0\ \forall\,\Delta>\Delta_0\ \exists\,\kappa,\{\tau_i\}:\quad \tau_i\ge 0,\quad \kappa\cdot\mu_\kappa=\sum_{i\in M}\tau_i,\quad a\equiv 1\ \text{is an equilibrium of (15)}.$$

The goal asserts the existence of a working scheme, as printed; it does not fix the scheme.

Milestones: Lemma B.1 (p. 38)

(a) For $\Delta>0$ and every $\phi$, $\phi_k\mapsto h(\phi_k;\phi)$ is continuous and weakly decreasing on $[0,\infty)$.

(b) For all sufficiently large $\Delta$ there is $\phi^*\ge 0$ with

$$h(\phi^*;\phi^*)=0,\qquad h(\phi_k;\phi^*)\ge 0\iff \phi_k\le\phi^*\quad(\phi_k\ge 0),$$

so that at the fee $\sum_i\chi_i/G(\phi^*)$ exactly the consumers with $\phi_k\le\phi^*$ pay.

Significance

Proposition 4.9 is the constructive half of the paper's message: an adoption failure driven by the split between who bears the cost and who reaps the benefit can be repaired without outside funding, by a fee on the side that benefits. The paper's scheme ($\tau_i=\chi_i$, $\kappa=\sum_i\chi_i/G(\phi^*)$) exactly reimburses adoption costs and is financed by a threshold set of consumers; Lemma B.1(b) is the fixed-point statement that makes this calibration consistent.

The result is proved in the paper (App. A.2, pp. 36–38, and App. B, pp. 38–41). It has no machine-checked proof. This mission produces one: a formal model of the access-fee mechanism in the reduced form the paper's proofs use, the threshold lemma, and the main proposition. The goal can be attacked through Lemma B.1(b) as in the paper, or by any other scheme meeting the definition.

Difficulty

The calibration is circular: the fee depends on the mass of paying consumers, and the mass of paying consumers depends on the fee. Lemma B.1(b) resolves this with a one-dimensional fixed point $h(\phi^*;\phi^*)=0$, and the delicate points are positivity of $G$ at the relevant arguments (so that the fee is finite), the three-piece shape of $h(\cdot;\phi)$, and choosing $\Delta$ large enough that the sign change happens inside the strictly decreasing piece. For the goal, the point to check is that the self-financing identity uses the actual mass of payers at the chosen fee: a fee too high drives the payers' mass, and with it the revenue, towards zero.

Formalization scope

• Reduced form. The paper's full model is a signal game with Bertrand pricing whose equilibrium concept is not defined precisely; its proofs work with the closed-form outcome of Proposition A.1. The formalization does the same: consumer utilities are those computed in the proof of 4.9 ($\Delta+L+h-\gamma$ with access, $\Delta/2+L+h-\gamma$ without), gross profit $\Pi$ is the constant $0$ in every profile (pp. 37–38, also for a deviating manufacturer), and "equilibrium" is a pure Nash equilibrium over unilateral switches of $a_i\in\{0,1\}$. Signal accuracy is $\alpha=1/2$, as in the paper's main text.
• Encoding. Manufacturers are Fin 2 × Bool × Fin m; adoption profiles are Bool-valued. $G$ is ProbabilityTheory.cdf μ for a measure μ on ℝ. $\Delta$ is an argument of every object, with $H=L+\Delta$.
• Standing assumptions (one predicate Model.Standing): $m\ge 2$, $0\le L$, $0\le l<h$, $\gamma>0$, $\chi_i>0$; $\mu$ a probability measure without atoms, $\mu((-\infty,0))=0$, and $\mu((a,b))>0$ for $0\le a<b$ (support $[0,\infty)$). No cost function $c_l$, no Assumption 1 and no finite mean are needed or assumed. Lemma B.1(a) additionally assumes $\Delta>0$, the model's $L<H$.
• Ties in the access decision go to paying, as in the proof's "$b_k=1$ iff $h\ge 0$".
• Ruled out. $\mu_\kappa$ is the $\mu$-measure of the paying consumers, not a free number in $[0,1]$; the equilibrium predicate and $\Pi$ are defined, not assumed; transfers are nonnegative; and no statement relies on Lean's value $0$ for a division by $G(\phi)=0$.
• Not formalized. The non-uniqueness clause of Lemma B.1(b) and Example B.1 (p. 40); the purchase-stage claims of the proof of 4.9 (market shares under transfers); Appendix C's symmetric-cost variant.
• Infrastructure. Only Mathlib's measure theory and ProbabilityTheory.cdf; no new library is needed. Lemmas on CDFs of atomless, fully supported laws on $[0,\infty)$ are reusable beyond this mission. Proofs of the milestones and of the goal are welcome; the goal may be proved by any route.

Selected references

• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, SSRN 3602376, version of 2022-08-19. https://ssrn.com/abstract=3602376
• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4532