All missions

Motivation

We prove that the center of each degenerate cyclotomic Hecke algebra associated to the complex reflection group of type B_d(l) consists of symmetric polynomials in its commuting generators. The classification of the blocks of the degenerate cyclotomic Hecke algebras is an easy consequence. We then deduce that the center of an integral block of parabolic category O for the Lie algebra gl_n(C) is generated by the center of its universal enveloping algebra.

This mission is the statement-level formalization of Centers of degenerate cyclotomic Hecke algebras and parabolic category O (arXiv:math/0607717v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Symmetric-polynomial center and explicit multipartition basis (Theorem 1, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

22 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 2: Integral parabolic category O and its natural center multiplication map (hard)
• Lemma 3.1: Filtered PBW symbol interface (hard)
• Theorem 3.2: Filtered PBW symbol interface (hard)
• Lemma 4.1: Generic complete-local deformation and modular dual Specht modules (hard)
• Lemma 4.2: Evaluation central characters and repeated shape-residue multisets (hard)
• Theorem 4.3: Primitive central idempotents and unital block corner centers (hard)
• Lemma 5.1: Ordered determinant central coefficients and actual comultiplication delta (hard)
• Lemma 5.2: Cyclic highest-weight modules and the concrete right affine-Hecke tensor action (hard)
• Corollary 5.3: Natural central and right Murphy actions in the same opposite endomorphism algebra (hard)
• Lemma 5.4: Character-difference multiset map and blockwise staircase multipartition map (hard)
• Lemma 5.5: Projective tensor modules for reordered compositions and action-compatible endomorphism isomorphism (hard)
• Theorem 5.6: Actual Schur-Weyl tensor representation and residue-selected block sum (hard)
• Corollary 5.7: Central determinant actions in the concrete tensor endomorphism algebra (hard)
• Lemma 5.8: Generalized-character tensor projection and represented block idempotent (hard)
• Corollary 5.9: Restricted block tensor action with center generators and O-simple count (hard)
• Lemma 5.10: Parabolic Verma flags and injective hulls internal to the O block (hard)
• Theorem 5.11: All three natural center maps and evaluation on the projected tensor module (hard)
• §1, unnumbered: central-character subcategories are blocks: Actual nonsplit-extension linkage in integral parabolic O (hard)
• §4, unnumbered: residue classification of blocks: Actual simple-module extension linkage and residue-selected block summands (hard)
• §4, unnumbered: central character of dual Specht modules: Modular induced dual Specht modules and their central actions (hard)
• §5, unnumbered: constituents of the projective tensor module: Simple highest-weight subquotients of the concrete projective tensor module (hard)
• §5, unnumbered: determinant translation to tensor blocks: Actual determinant tensor functor and transported central-character action (hard)

Selected references

• Centers of degenerate cyclotomic Hecke algebras and parabolic category O, arXiv:math/0607717v3, https://arxiv.org/abs/math/0607717v3

Motivation

We give the first composable security proof for continuous-variable quantum key distribution with coherent states against collective attacks. Crucially, in the limit of large blocks the secret key rate converges to the usual value computed from the Holevo bound. Combining our proof with either the de Finetti theorem or the Postselection technique then shows the security of the protocol against general attacks, thereby confirming the long-standing conjecture that Gaussian attacks are optimal asymptotically in the composable security framework. We expect that our parameter estimation procedure, which does not rely on any assumption, will find applications elsewhere, for instance for the reliable quantification of continuous-variable entanglement in finite-size settings.

This mission is the statement-level formalization of Composable security proof for continuous-variable quantum key distribution with coherent states (arXiv:1408.5689v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 7: Haar complex half-projection norm concentration (Lemma 7, E2–E3, PDF p. 20). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

17 results of the paper are not stated yet, because the library lacks an interface they need:

• Seed paper result pinned to Theorem 1: collective-attack composable security: Complete finite-precision E0 CPTP protocol and full transcript leakage/error budget (source-ambiguity)
• Theorem 2: PE acceptance and Holevo underestimation: Outcome-indexed residual quantum state and PE underestimation event (source-ambiguity)
• Theorem 3: appendix restatement of the finite-key security bound: Complete finite-precision E0 CPTP protocol and full transcript leakage/error budget (source-ambiguity)
• Theorem 4: AEP for a conditional state: Separable-memory optimized purified-distance smooth conditional min-entropy and actual commuting postselection (hard)
• Theorem 12: virtual-PE bad-event union bound: Well-defined conditioning and valid nonnegative-variable application for signed correlations (source-ambiguity)
• Corollary 13: PE passes but Eve information is underestimated: The same actual PE residual-state bad-event probability space as Theorem 2 (source-ambiguity)
• Unnumbered main result: asymptotic Gaussian Holevo key rate: Complete protocol family with discretization, reconciliation, transcript and robustness limit (source-ambiguity)
• Unnumbered main result: general-attack upgrade: Instantiated CV energy-test/postselection protocol, dimension, shortening and joint budget (source-ambiguity)
• Appendix G: direct reconciliation without active symmetrization: Complementary cross energy-test instruments and combined key operation (source-ambiguity)
• Unnumbered result: coherent-state PM/EB equivalence: One consistent TMSV/coherent/heterodyne quadrature and modulation normalization (source-ambiguity)
• Unnumbered result: PE simulation without optical symmetrization or extra parties: Exact virtual-PE simulation algorithm, output law and complexity model (source-ambiguity)
• D24–D25: positive AEP correction with lower-bounded passing probability: The same complete separable-memory postselection entropy interface, at block size 2n (hard)
• D30–D33: entropy inference conditioned on acceptance: Consistent conditional word entropy normalization and concentration failure parameter (source-ambiguity)
• D34–D38: Gaussian phase invariance and three-parameter heterodyne Holevo comparison: Actual two-mode Gaussian purification, continuous heterodyne instrument and measured Eve Holevo comparison (hard)
• E63: Holevo bound after PE acceptance: Outcome-indexed Holevo quantity after PE acceptance, not fixed-state exceptional probability (source-ambiguity)
• F6: smooth min-entropy bound after EC and PE acceptance: Complete accepted-protocol conditional cq entropy and full transcript leakage accounting (source-ambiguity)
• Appendix C: expected rate and claimed 0.99 robustness: Rigorous joint robustness quantile and consistent SNR/key-length model (source-ambiguity)

Selected references

• Composable security proof for continuous-variable quantum key distribution with coherent states, arXiv:1408.5689v3, https://arxiv.org/abs/1408.5689v3

Communication in two-sided marketplaces

A platform may know the services its users seek and offer while still lacking the preferences that determine whether a particular match is worthwhile. Learning those preferences requires communication. A lower bound on that communication would distinguish a limitation of one search algorithm from a limitation shared by every platform design. Peng Shi's Optimal Matchmaking Strategy in Two-Sided Marketplaces studies this question through assignment markets with privately known benefits and costs. The present target is Proposition 12, which supplies the communication lower bounds summarized in the paper's Table 4. Its two numbered supporting lemmas are included; independent upper bounds are outside this mission.

The targets preserve the source's literal communication model. A finding about that model is consequential: observing boundaries between arbitrarily short messages can reveal information that is not charged as bits. The printed unrestricted lower bounds and their supporting information lemmas are therefore retained as source claims to be assessed, rather than presented as established machine-checked results. The detailed counterexamples and source locations accompany the mission in its findings.

Assignment outcomes and private messages

An assignment game has a set of customers $I$ and a distinct set of providers $J$, both of size $n$. Customer $i$ receives benefit $b_{ij}$ from provider $j$'s service, whose cost is $c_{ij}$. Each agent can have at most one partner. A transaction outcome consists of a binary matching $x$ and real prices $p_i$ paid by customers. Unmatched customers pay zero. In a matched pair, the customer's surplus is $u_i=b_{ij}-p_i$ and the provider's is $v_j=p_i-c_{ij}$; unmatched agents have zero surplus.

For a tolerance $\epsilon>0$, an outcome is $\epsilon$-stable when every agent's surplus is nonnegative and

$$u_i+v_j+2\epsilon\ge b_{ij}-c_{ij}\qquad(i\in I,\ j\in J).$$

The condition concerns every pair, including pairs absent from the matching. It expresses that a pair cannot deviate and improve both participants' surpluses by more than $\epsilon$. These are the transaction and stability conventions of §§2.1–2.3, pages 7–9 of the supplied artifact.

The binary market $M(n,d^I,d^J)$ draws every benefit independently as $.99$ with probability $d^I$, and zero otherwise. Independently, every cost is $.01$ with probability $d^J$, and one otherwise. Customer $i$ initially knows only her benefit row; provider $j$ knows only his cost column. The distributions and market size are public. A blackboard protocol starts with a fixed speaker. Each message is a finite binary string determined by its sender's private input and the history of complete messages. A public deterministic controller uses that history to select the next speaker or terminate with a transaction outcome.

Only the bits in the messages are charged. Messages may be empty, and there is no limit on rounds or computation. Protocols must terminate on every supported input. The per-agent communication cost is the maximum total bit count on this support divided by $2n$. A one-round protocol requires each agent's single message to depend only on that agent's private input, with the output determined by the tuple of messages. These definitions follow Definitions 3–5, pages 23–25.

Formalization targets

Proposition 12 asserts the existence of universal constants $\kappa_1,\kappa_2,\kappa_3>0$. For every $n\ge64$ and $0<\epsilon<.49$, a protocol with probability at least $.99$ of returning an $\epsilon$-stable outcome must satisfy all applicable bounds:

$$\begin{aligned} \operatorname{cost}(P)&\ge\kappa_1\log n &&\text{in }M(n,1/n,1),\\ \operatorname{cost}(P)&\ge\kappa_2/d^J &&\text{in }M(n,1/(nd^J),d^J),\quad d^J\in[1/\sqrt n,1/2],\\ \operatorname{cost}(P)&\ge\kappa_3\log n &&\text{in }M(n,.5,.5)\text{ for one-round }P. \end{aligned}$$

The constants precede all market and protocol quantifiers. The entire conjunction is the goal, as printed on page 26.

For the milestones, let $\Pi$ be the concatenation of all bits communicated before termination. A pair is good when its benefit is $.99$ and cost $.01$, and perfect when it is good and no other good pair shares either endpoint. Write their indicators as $G_{ij},P_{ij}$, and let $x_{ij}$ be the run's output matching indicator. A low-error pair satisfies

$$\mathbb E[P_{ij}(1-x_{ij})+(1-G_{ij})x_{ij}]\le .04/n.$$

The expectation is unconditional; the set of low-error pairs is fixed before the profile is sampled.

Lemma D.3, page 43, considers the laws $\pi_{11},\pi_{10},\pi_{01},\pi_{00}$ of $\Pi$ conditional on the pair's two flags. In the second market regime it asserts

$$\tfrac12\|\pi_{11}-\pi_{00}\|_1\le\|\pi_{10}-\pi_{00}\|_1+\|\pi_{01}-\pi_{00}\|_1.$$

Here the norm is the full sum of absolute mass differences. The formal statement covers every protocol and pair in that regime, so it specializes to the successful protocol and low-error pair in the source's application.

Lemma D.2, page 41, fixes a low-error pair in a protocol with success probability at least $.99$ and $d^Id^J=1/n$. It asserts both strict inequalities:

$$I(b_{ij},c_{ij};\Pi)>.05\log_2(n)/n\quad(d^J=1),$$ $$I(b_{ij},c_{ij};\Pi)>.0004/(nd^J)\quad(d^J\in[1/\sqrt n,1/2]).$$

Mutual information is measured in bits. The milestone order is D.3, then D.2; the one-round clause uses the separate argument in Appendix D.6.

Significance and status

The claimed bounds distinguish markets where one side has easy-to-describe preferences, sparse reciprocal interest, and simultaneous communication. In particular, setting $d^J=1/\sqrt n$ in the second clause gives the claimed square-root worst-case scale. Their universal protocol quantifiers are central to the paper's near-optimality comparison.

The formalization makes the protocol's information access, transfer feasibility, and cost accounting explicit. Its general communication and assignment objects are reusable independently of the binary market. Definitions are concrete, and the theorem declarations are unproved statement targets. Compilation checks their well-formedness; it does not establish their truth. The literal-model finding remains relevant to resolving those targets.

The coding-model difficulty

The observable message history and its flattened bit transcript are different random variables. The source defines the latter explicitly in Appendix D.5, but treats it as if it also determines the output and has the information properties of a fully observable history. Under Definition 3, arbitrary empty messages can encode private information at no additional bit cost. The recorded instance yields cost one and exact stability, while its concatenated transcript is constant. This contradicts the unrestricted claims and the positive information bounds. A related instance makes the rectangle inequality read $1\le0$.

Adding prefix-free or nonempty-message restrictions would change the targets' domain. The mission therefore retains the printed class and records the defect. This finding does not disprove the one-round clause. Separately, the proof's use of $L/n$ conflicts with Definition 3's $L/(2n)$; the formal cost follows the definition.

Formalization scope

The two populations are tagged copies of Fin n. Boolean profiles are exact encodings of the binary preferences, while prices, tolerance, and density parameters remain real. The distribution is its full independent product mass. Finite sums compute probabilities, conditional laws, and mutual information over the distinct transcript values. Zero-mass profiles affect neither probability nor the supported maximum cost. All conditioning events used in D.3 are positive.

The controller observes lists of messages, and outcomes are computed from actual terminating runs. No entropy bound, factorization property, or transcript decoder is an admissibility assumption. Natural logarithms in Proposition 12 only rescale its existential constants; D.2 uses base two with its exact explicit constants. Every $n\ge64$ and both density interval endpoints are included.

Selected references

• Peng Shi, Optimal Matchmaking Strategy in Two-Sided Marketplaces, Management Science, 2023. DOI: 10.1287/mnsc.2022.4444. Published citation basis; supplied 65-page artifact, Proposition 12 on page 26 and Lemmas D.2–D.3 on pages 41 and 43. PDF and printed page numbers coincide.

Why characterize the Shannon entropy

The Shannon information function $H(p) = -\sum_i p_i \ln p_i$ measures the average information gained when one samples a discrete probability distribution $p$. Its use as a measure of distinguishability (the mutual information of Chapter 2 of C. A. Fuchs's thesis, arXiv:quant-ph/9601020) is only as convincing as the reasons for the formula itself. Section 2.4.1 of the thesis derives the formula from two requirements on an information function: it depends only on the probabilities and not on how outcomes are labelled (symmetry), and the expected information gained does not depend on the order in which an observer asks about the outcome (objectivity). The derivation follows Z. Daróczy (Information and Control 16, 1970), who embeds the problem in a one-parameter family of functional equations whose solutions are explicit, and recovers Shannon's formula as the limit $\alpha \to 1$.

Characterizations of this kind go back to Shannon (1948), Khinchin (1953) and Faddeev (1956), who used continuity or monotonicity assumptions. Daróczy's route needs no regularity hypothesis on $H$ at all: symmetry and the recursion of type $\alpha$ already force a closed form, and the regularity enters only through the limit in $\alpha$. This mission formalizes that derivation as Fuchs presents it (Theorem 2.7, printed pp.32–35).

Setting

For $n \ge 1$ let

$$\Gamma_n = \Big\{ (p_1,\dots,p_n) \;\Big|\; p_k \ge 0,\ \sum_{i=1}^n p_i = 1 \Big\}$$

be the $n$-point probability distributions and $\Gamma = \bigcup_n \Gamma_n$. In Lean, IsDist p says that p : Fin n → ℝ lies in $\Gamma_n$.

A function $H : \Gamma \to \mathbb R$ is a family $H_n$ of functions of $n$ real arguments. It is symmetric (IsSymmetric H) if $H(p_{\sigma(1)},\dots,p_{\sigma(n)}) = H(p_1,\dots,p_n)$ for every permutation $\sigma$ and every $p \in \Gamma_n$.

Fix a real parameter $\alpha > 0$, $\alpha \ne 1$. A function $H_\alpha$ satisfies the recursion of type $\alpha$ (SatisfiesRecursion α H), Eq. (2.111), if for every $n \ge 2$ and $p \in \Gamma_n$ with $p_1 + p_2 > 0$,

$$H_\alpha(p_1,\dots,p_n) = H_\alpha(p_1+p_2, p_3,\dots,p_n) + (p_1+p_2)^{\alpha}\, H_\alpha\!\Big(\frac{p_1}{p_1+p_2}, \frac{p_2}{p_1+p_2}\Big).$$

At $\alpha = 1$ this is the objectivity requirement (2.110). Throughout the proof, $f(x) = H_\alpha(x, 1-x)$ for $0 \le x \le 1$ (2.114), and $s_i = p_1 + \dots + p_i$.

Formalization targets

Goal: Theorem 2.7 (Daróczy)

Let $(H_\alpha)_{\alpha > 0,\ \alpha \ne 1}$ be symmetric solutions of the recursion of type $\alpha$, and suppose $H_\alpha(\tfrac12,\tfrac12) \to C$ as $\alpha \to 1$. Then for every $n$ and $p \in \Gamma_n$,

$$\lim_{\alpha \to 1} H_\alpha(p_1,\dots,p_n) = -\frac{C}{\ln 2}\sum_{i=1}^n p_i \ln p_i, \qquad 0 \ln 0 = 0.$$

The constant $C$ fixes the units: $C = 1$ for bits, $C = \ln 2$ for nats.

Milestones (fixed $\alpha > 0$, $\alpha \ne 1$; $H_\alpha$ symmetric and satisfying (2.111))

1. (2.115) $H_\alpha(p_1,\dots,p_n) = \sum_{i=2}^n s_i^\alpha f(p_i/s_i)$.
2. (2.119) $f(x) + (1-x)^\alpha f\big(\tfrac{y}{1-x}\big) = f(y) + (1-y)^\alpha f\big(\tfrac{x}{1-y}\big)$ for $x, y \in [0,1)$, $x + y \le 1$.
3. (2.120) $f(0) = f(1) = 0$.
4. (2.122) $F(p,q) = f(p) + [p^\alpha + (1-p)^\alpha] f(q)$ satisfies $F(p,q) = F(q,p)$ on $[0,1]^2$.
5. (2.124) $f(p) = C(2^{1-\alpha}-1)^{-1}[p^\alpha + (1-p)^\alpha - 1]$ on $[0,1]$, $C = f(\tfrac12)$.
6. (2.130) $H_\alpha(p) = C(2^{1-\alpha}-1)^{-1}\big(\sum_{i=1}^n p_i^\alpha - 1\big)$ on every $\Gamma_n$, $C = H_\alpha(\tfrac12,\tfrac12)$.

Significance

The result singles out the Shannon entropy among all symmetric information functions by a purely algebraic requirement, with no continuity, monotonicity or measurability assumption on $H_\alpha$. Milestone (2.130) is of independent interest: it shows that the symmetric solutions of the recursion of type $\alpha$ are exactly the multiples of the Daróczy information of type $\alpha$, $(2^{1-\alpha}-1)^{-1}(\sum_i p_i^\alpha - 1)$ (known in physics as the Tsallis entropy), which is related to the Rényi information of order $\alpha$ by (2.132). The goal then identifies the Shannon entropy as its $\alpha \to 1$ limit, which fixes the information function used for the mutual-information distinguishability measure in the rest of the thesis.

The theorem is classical and its proof in the thesis is complete; none of these statements is formalized on the platform, and Mathlib contains the Shannon entropy only in the form of Real.negMulLog and binary entropy, without a characterization theorem. This mission produces a machine-checked characterization of the Shannon and Daróczy entropies from symmetry and recursivity, reusable by any development that needs to justify an entropy formula axiomatically.

Difficulty

Each step is elementary, but several are easy to get wrong. The reduction (2.115) iterates the recursion, which only applies when the first two entries are not both zero; distributions that begin with zeros must first be permuted using symmetry. The symmetry of $F$ (2.122) needs the substitution $p = 1 - x$, $q = y/(1-x)$ and then a second substitution $z = (1-p)/(1-pq)$ (2.127), each valid only away from the endpoints, so the boundary cases $p, q \in \{0, 1\}$ must be handled separately with $f(0) = f(1) = 0$. The final limit is a $0/0$ form in $\alpha$; the thesis applies l'Hôpital's rule (its display (2.131) prints $\alpha \to 0$, a misprint for $\alpha \to 1$), and entries $p_i = 0$ must be checked to contribute $0$ on both sides.

Formalization scope

• A function on $\Gamma$ is H : (n : ℕ) → (Fin n → ℝ) → ℝ; its values off $\Gamma_n$ are irrelevant. The family in the goal is H : ℝ → (n : ℕ) → (Fin n → ℝ) → ℝ, with symmetry and the recursion assumed for every $\alpha > 0$, $\alpha \ne 1$.
• Indices are 0-based: the source's $p_1, p_2$ are p 0, p 1, and the merged vector $(p_1+p_2, p_3,\dots,p_n)$ is Fin.cons (p 0 + p 1) (fun i => p i.succ.succ).
• The recursion is required only where its right side is defined, $p_1 + p_2 > 0$; Lean's 0 / 0 = 0 imposes no extra condition on $H$.
• Powers are Real.rpow, so $0^\alpha = 0$ for $\alpha > 0$; logarithms are natural (Real.log), and Real.log 0 = 0 gives $0 \ln 0 = 0$.
• The limit is along 𝓝[≠] 1. "Up to a constant $C$" is read as: if $H_\alpha(\tfrac12,\tfrac12) \to C$ then $H_\alpha(p) \to -(C/\ln 2)\sum_i p_i \ln p_i$; a family with constant $H_\alpha(\tfrac12,\tfrac12) = C$ is a special case.
• A trivial formalization is ruled out: the hypotheses are satisfied by the nonzero Daróczy family for every $\alpha$ (checked in a verification file), and the constant function $1$ violates the recursion.

Needed infrastructure: finite sums over Fin n with Fin.cons/Fin.succ reindexing, permutations of Fin n, Real.rpow identities $(st)^\alpha = s^\alpha t^\alpha$ for $s, t \ge 0$, and one-sided derivatives of $\alpha \mapsto a^\alpha$ for the limit. Proofs of any milestone, and alternative routes to the goal through (2.130), are welcome.

Selected references

• C. A. Fuchs, Distinguishability and Accessible Information in Quantum Theory, PhD dissertation, University of New Mexico, 1995. arXiv:quant-ph/9601020v1
• Z. Daróczy, Generalized information functions, Information and Control 16 (1970) 36–51. doi:10.1016/S0019-9958(70)80040-7
• J. Aczél and Z. Daróczy, On Measures of Information and Their Characterizations, Academic Press, 1975.
• C. E. Shannon, A mathematical theory of communication, Bell System Technical Journal 27 (1948) 379–423. doi:10.1002/j.1538-7305.1948.tb01338.x

Motivation: paying for honest probabilities

A forecaster, an economist or any expert who sells a probability distribution cannot be checked directly: a single outcome of an experiment never reveals whether the reported distribution was the expert's true state of knowledge. The only safeguard is to pay according to a scheme under which lying does not pay in expectation. This is the problem of keeping the expert honest, studied in the statistics and decision-theory literature on proper scoring rules (Good 1952; McCarthy 1956; Savage 1971; Aczél and Pfanzagl 1966).

Chapter 2 of C. A. Fuchs's thesis Distinguishability and Accessible Information in Quantum Theory (arXiv:quant-ph/9601020) uses this problem to derive a measure of distinguishability of probability distributions. If honesty is enforced by an optimal payment scheme, the expected loss an expert suffers by reporting $p_1$ instead of his true $p_0$ measures how far apart the two distributions are. Aczél's theorem (Theorem 2.3 of the thesis, p.21) says that for three or more outcomes the optimal schemes are exactly the logarithmic ones, and the expected loss is then the Kullback–Leibler relative information $K(p_0/p_1)=\sum_b p_0(b)\ln\big(p_0(b)/p_1(b)\big)$, eq. (2.76). This mission formalizes that theorem and its proof as given on pp.20–24 of the thesis.

Setting

An experiment has outcomes $k = 1, \dots, n$. A strictly positive $n$-point distribution is a vector $p=(p_1,\dots,p_n)$ with every $p_k>0$ and $\sum_k p_k=1$ (IsPosDist). An expert whose knowledge is $p$ reports a distribution $q$ and is paid $F_k(q_k)$ when outcome $k$ occurs, where $F_1,\dots,F_n$ are fixed real functions chosen in advance. His expected earnings are $\sum_k p_k F_k(q_k)$.

The family $F$ keeps the expert honest (KeepsHonest F) if

$$\sum_{k=1}^{n} p_k F_k(q_k)\;\le\;\sum_{k=1}^{n} p_k F_k(p_k)\qquad(2.47)$$

for every pair of strictly positive $n$-point distributions $p,q$: telling the truth maximizes expected payment.

Formalization targets

Goal: Theorem 2.3 (Aczél)

For $n\ge 3$,

$$\texttt{KeepsHonest}\,F\iff\exists\,\alpha\ge 0,\ \exists\,\gamma_1,\dots,\gamma_n:\quad F_k(p)=\alpha\ln p+\gamma_k\ \text{ for all } k \text{ and all } p\in(0,1).$$

The printed theorem allows any constant $\alpha$; the "if" direction is false for $\alpha<0$, and the statement here carries the correction $\alpha\ge 0$, which the thesis's own proof derives.

Milestones

The milestones follow the proof on pp.21–24, for any two distinct outcomes $i\ne j$ (the page's outcomes 1 and 2):

1. (2.50): for $0<p,q<r<1$, $\;pF_i(q)+(r-p)F_j(r-q)\le pF_i(p)+(r-p)F_j(r-p)$.
2. (2.54)–(2.56): every $F_k$ is nondecreasing on $(0,1)$.
3. (2.61)–(2.62), corrected: the difference quotient $\frac{F_i(p)-F_i(q)}{p-q}$ lies between $\frac{r-p}{p}D_j$ and $\frac{r-q}{q}D_j$, where $D_j$ is the difference quotient of $F_j$ between $r-q$ and $r-p$; the order of the two bounds depends on the sign of $p-q$.
4. (2.66): if $F_j$ is differentiable at $r-p$, then $F_i$ is differentiable at $p$ and $pF_i'(p)=(r-p)F_j'(r-p)$.
5. Lemma 2.1 (Lebesgue): a nondecreasing function on $[a,b]$ is differentiable almost everywhere, its derivative is measurable, and $\int_a^b f'\le f(b)-f(a)$.
6. (2.67)–(2.69): $F_i(p)=\alpha\ln p+\gamma_i$, $F_j(p)=\alpha\ln p+\gamma_j$ on $(0,1)$ with a common $\alpha\ge 0$.
7. (2.70): the Shannon inequality $\sum_k p_k\ln q_k\le\sum_k p_k\ln p_k$, with equality iff $p=q$, which gives the "if" direction.

Significance

The theorem singles out the logarithmic payoff from an incentive requirement alone, without any appeal to additivity or to axioms about information. In the thesis it is the route from a decision problem to the Kullback–Leibler information (2.76), one of the classical distinguishability measures that Chapter 3 then optimizes over quantum measurements. The same characterization underlies the uniqueness of the logarithmic scoring rule among local proper scoring rules, a standard fact in forecast evaluation and in the theory of elicitation.

The result is classical and proved; this mission produces a machine-checked version of it. Neither Aczél's characterization nor the specific chain (2.50)–(2.69) is on the platform. Mathlib has Lebesgue's differentiation theorem for monotone functions and Gibbs-type inequalities; the platform has Gibbs' inequality without its equality case (gibbs_inequality) and the almost-everywhere differentiability of globally monotone functions (FamousTheorems.lebesgue_monotone_differentiation_6b), but neither in the form stated here.

Difficulty

The "if" direction is a short convexity argument. The difficulty is the "only if" direction: nothing is assumed about the $F_k$, not continuity and not measurability, so regularity must be extracted from the inequality itself. Monotonicity follows by combining two instances of (2.50). Differentiability is the delicate step. The sandwich (2.61)–(2.62) only transfers differentiability from $F_j$ at $r-p$ to $F_i$ at $p$; one needs a point of differentiability of $F_j$ to start from, which is where Lebesgue's theorem enters, and the freedom to move $r$ through $(p,1)$, which is exactly what $n\ge 3$ provides. For $n=2$, $r$ is pinned to $1$ and the theorem fails: Muszély's family (2.75) gives many non-logarithmic honest payoffs. The natural first idea, differentiating (2.47) in $q$ at $q=p$ with Lagrange multipliers, presupposes the differentiability that has to be proved.

Formalization scope

• Outcomes are Fin n; payoffs are F : Fin n → ℝ → ℝ; $\ln$ is Real.log.
• Distributions are strictly positive. The source declares $F_k$ on $[0,1]$, but (2.48) is undefined at $0$, and with real values $F_k(0)$ and distributions with zero entries only constant payoffs would be honest, contradicting the theorem's own "if" direction. With $n\ge 3$ every coordinate of a positive distribution lies in $(0,1)$, so $F_k$ is constrained exactly on $(0,1)$ and (2.48) is asserted there.
• $\alpha\ge 0$ is part of the goal (correction; counterexample $\alpha=-1$, $p=(\tfrac12,\tfrac14,\tfrac14)$, $q=(\tfrac13,\tfrac13,\tfrac13)$). $\alpha=0$, constant payoffs, is a genuine solution and is allowed.
• Printed (2.61)–(2.62) divide by $p-q$ without tracking its sign; the milestone states both cases.
• Lemma 2.1 states the integrability of $f'$ explicitly, so the integral bound is not met by Lean's default value $0$ for a non-integrable integrand.
• Every theorem item lists its differences from the source at the end of its statement.

Contributions welcome: proofs of the milestones, in particular a reusable Lebesgue-type lemma for functions monotone on an interval and the transfer argument (2.66); the Shannon inequality with equality case is reusable well beyond this mission.

Selected references

• C. A. Fuchs, Distinguishability and Accessible Information in Quantum Theory, PhD thesis, University of New Mexico, 1995. arXiv:quant-ph/9601020
• J. Aczél and J. Pfanzagl, Remarks on the measurement of subjective probability and information, Metrika 11 (1966) 91–105. doi:10.1007/BF02613579
• J. Aczél and Z. Daróczy, On Measures of Information and Their Characterizations, Academic Press, 1975.
• L. J. Savage, Elicitation of personal probabilities and expectations, J. Amer. Statist. Assoc. 66 (1971) 783–801. doi:10.1080/01621459.1971.10482346
• H. L. Royden, Real Analysis, 3rd ed., Macmillan, 1988, p.96 (Lebesgue's theorem).

Motivation

Allocating scarce vaccines, ventilators, or antiviral treatments can involve several ethical priorities at once. A reserve system attaches a quota to each category and gives that category its own ordering of eligible patients. Categories can express different claims on the same supply without making the medical units physically different. The mathematical question is which assignments simultaneously honor eligibility, avoid leaving a usable unit idle, and respect the applicable priorities. This mission concerns the deferred-acceptance characterization in Pathak, Sönmez, Ünver and Yenmez, arXiv:2008.00374v3, §§3.1–3.5, pp. 13–18.

A single ranking of patients need not express the priorities of every category. The model therefore allows category orders to differ independently. It also records the category through which a patient receives a unit. That information matters even when all units provide the same benefit: it identifies which quota was used and which priority order governed the assignment. The source explains this distinction in §3.2, pp. 13–14.

Setting

There is a finite set of patients $I$ and a finite set of categories $C$. Category $c$ has a natural-number quota $r_c$, with total supply $q=\sum_{c\in C}r_c$. Its priority order $\pi_c$ is a strict linear order on $I\cup\{\varnothing\}$. The distinguished outside option $\varnothing$ determines eligibility: patient $i$ is eligible for category $c$ exactly when $i\pi_c\varnothing$. Categories may have overlapping eligible populations, independent priorities, or zero quotas. No scarcity inequality between supply and population size is assumed.

A matching is a function $\mu:I\to C\cup\{\varnothing\}$ such that $|\mu^{-1}(c)|\le r_c$ for every category. Each patient receives at most one unit, and $\mu(i)=\varnothing$ means that patient is unmatched. Membership in the set $M$ of matchings imposes capacity alone. Eligibility is a separate axiom.

The source specifies three requirements. Compliance with eligibility requires every assigned patient to be eligible at her assigned category. Non-wastefulness requires a category to be full whenever an eligible patient is unmatched. Respect for priorities requires every patient assigned to a category to outrank every unmatched patient in that category's full order. This last requirement compares recipients with unmatched patients, including ineligible unmatched patients; it does not compare all pairs of patients assigned to different categories. These are Definitions 1–3, pp. 14–15.

An artificial preference profile assigns each patient a strict order $\succ_i$ on $C\cup\{\varnothing\}$, with $c\succ_i\varnothing$ exactly when $i$ is eligible at $c$. The set of all such compatible profiles is $\mathcal P$. These auxiliary orders may differ across patients; they do not describe differing values for the identical medical units.

The individual-proposing deferred-acceptance algorithm, abbreviated DA, begins with no patient held. Free patients apply to their highest-ranked untried eligible category. In each simultaneous round a category considers both its current incumbents and its new applicants, retains its highest-priority quota-many patients, and rejects the rest. Rejected patients continue down their lists. The source stops when a round makes no rejections and finalizes the holds. A matching is DA-induced when it is the output for some profile in $\mathcal P$; see §3.5, pp. 17–18.

Formalization target

The single target is the complete statement of Proposition 1, printed/PDF p. 18 of arXiv:2008.00374v3. For every reserve system $R$ and every capacity-feasible matching $\mu$,

$$\begin{aligned} &\bigl[\mu\text{ complies with eligibility}\bigr] \land\bigl[\mu\text{ is non-wasteful}\bigr] \land\bigl[\mu\text{ respects priorities}\bigr]\\ &\qquad\Longleftrightarrow \exists\succ\in\mathcal P,\quad\operatorname{DA}(R,\succ)=\mu. \end{aligned}$$

Equality here is equality of the whole assignment function, including the category assigned to every recipient. Both directions and all three axioms belong to the same target. There are no numbered supporting milestones: the proof in Appendix C.2, printed A.13–A.14 / PDF pp. 57–58 uses the definitions directly.

Significance

The characterization connects an axiomatic description of acceptable assignments with a concrete allocation procedure. It identifies exactly the assignments reachable as the auxiliary preference profile varies, rather than merely establishing existence of one acceptable assignment. Independence of category priorities preserves the possibility that different categories express different allocation criteria.

The paper supplies a mathematical proof. This mission provides its Lean statement and the definitions needed to formalize that proof; the goal is not yet proved in Lean. The general finite admissions market, assignment type, and simultaneous DA procedure are reused from published definition modules. The additional definitions expose the reserve model's full priorities, its three axioms, and the conversion to algorithm inputs. A completed proof would verify this connection while retaining zero quotas, partial eligibility, and arbitrary finite sizes.

Difficulty

The operational output and the axiomatic description express different kinds of information. A run records applications, rejections, and temporary holds; the axioms concern the final matching. Categories may displace incumbents, priorities may conflict across categories, and eligibility can exclude some pairs. These features make it necessary to track the actual simultaneous procedure faithfully.

The converse demands a realizing compatible profile for each prescribed matching satisfying the axioms. Producing an arbitrary fair matching, or only the same set of recipients, would not meet that requirement. Likewise, replacing respect for priorities by a familiar stability predicate would alter the target. These distinctions are present in the model and Proposition 1, pp. 13–18.

Formalization scope

Patients and categories use Fin n and Fin m with arbitrary cardinalities, and Option supplies the outside option. Full strict orders are rank bijections, with smaller ranks better. This retains every order, including ranks below the outside option. Supply is defined as the sum of the quotas, eliminating a redundant parameter. Empty populations are included as a boundary generalization; every source instance remains available.

The published assignment type is combined with a separate capacity predicate. Published admissions feasibility and stability predicates do not replace the source's axioms. The adapter sorts the eligible restrictions of the full orders into acceptable lists. For compatible profiles, mutual-acceptability filtering removes no pair. The published recursion uses the number of permissible pairs as fuel and pads stationarily after termination; its terminal assignment agrees with the source's no-rejection stop convention. This is an encoding convention, not an additional hypothesis or a numerical bound asserted by Proposition 1.

DA-induced is defined using the computed output, never by choosing an assignment already satisfying the axioms. No algorithm-correctness or preference-realization fact is supplied as model data. The mission excludes the separate cutoff-equilibrium characterization, sequential-reserve comparative statics, and smart-reserve results. Work on the complete proof and its necessary internal invariants is within scope.

Selected references

• Parag A. Pathak, Tayfun Sönmez, M. Utku Ünver and M. Bumin Yenmez, Fair Allocation of Vaccines, Ventilators and Antiviral Treatments: Leaving No Ethical Value Behind in Health Care Rationing, preprint arXiv:2008.00374v3, 1 July 2023, draft dated May 2023. Pinned source. Model: §§3.1–3.3, pp. 13–15; target and algorithm: §3.5, pp. 17–18; proof: Appendix C.2, printed A.13–A.14 / PDF pp. 57–58. All numbering in this mission refers to this preprint version.

Learning prices and inventory together

A retailer selling perishable products must choose both a selling price and an inventory position. The two decisions affect sales, spoilage, stock carried to the next period, and the information available for future decisions. Demand parameters may change during the selling horizon, while the distribution of demand disturbances and the distribution of perishability are initially unknown. The paper of Keskin, Li and Song proposes policies that combine price experimentation, statistical estimation, and change detection. This mission concerns its stated regret guarantees for both policies, including the intermediate results used in their analysis.

The stochastic inventory model

There are $T$ selling periods. A history policy chooses a real price $p_t$ and a real order-up-to level $y_t$ using past observed demands, perished proportions, and actions. Prices and inventory positions belong to nondegenerate compact intervals $P$ and $Y$ with positive endpoints. Replenishment has zero lead time and no fixed ordering charge. Unmet demand is lost but observed.

Demand is $D_t=g(\alpha_t+\beta_t p_t)+\varepsilon_t$. The known link $g$ is increasing and twice continuously differentiable. The unknown pair $\theta_t=(\alpha_t,\beta_t)$ lies in a compact rectangle with negative price coefficient. It has $C$ change points; distinct parameter values are separated by a positive distance. There is no minimum duration for a constant segment. The disturbances are independent and identically distributed, centered, and have a bounded second moment and a local moment generating function bound. Their distribution may have atoms. A separate independent sequence of perished proportions has a beta distribution with an unknown, time-independent parameter in a positive compact rectangle.

Inventory evolves according to $x_{t+1}=[(1-q_t)y_t-D_t]^+$. A feasible decision satisfies $y_t\ge x_t$. Known nonnegative holding, lost-sales, disposal, and ordering costs are denoted by $h,b,w,c$. The standing restriction is $|h-c|<b+p$ for every allowed price. The single-period expected profit $Q$ is defined by the actual cost integrals in equations (4)–(5), including perishability and both positive-part losses.

The full-information anticipatory benchmark, or FIA, knows the complete deterministic parameter sequence and the primitive laws, but cannot observe future shocks. It maximizes the expected total reward in equation (3), including terminal salvage. The paper explicitly assumes an interior optimal solution exists. Learner and benchmark have separate inventory trajectories on common primitive shocks. Their regret is the expectation of the signed sum of their single-period profit differences.

Formalization targets

The principal target is both clauses of Theorem 1 in the supplied paper:

$$\Delta_N(T)\le K_1 T^{2/3}\sqrt{\log T},\qquad \Delta_E(T)\le K_2\sqrt T\log T\quad(T=3,4,\ldots).$$

Each constant is positive, finite, and chosen before the horizon and the allowable locations and values of the changes. Constants may depend on the fixed change-count bound, model bounds, noise law, separation, and policy tuning. The learner's rules are chosen before the unknown noise law, change count, separation, and environment. The conclusion includes their executability; the theorem does not assume away failed constructions.

Both policies alternate experimentation and profit maximization. Their experimental lengths and cycle lengths are the printed ceiling formulas. Experimental observations support demand quasi-likelihood estimation, beta maximum likelihood estimation, and change detection. Demand estimation uses observations since the last detected change; perishability estimation uses all past experimental observations. DDPO-N optimizes a residual-based empirical profit on a sparse price grid. DDPO-E fits a known exponential family and optimizes its estimated profit over the full continuous price interval. Both then apply the printed inventory adjustment.

The eleven milestones are Proposition 1, comparing FIA with the full-information non-anticipatory policy; Propositions 2–3 on parameter estimation; Lemmas EC.2 and EC.1 on noise moments, sample-cost tails, and optimal inventory; Propositions 4–7 on the two profit proxies and the pricing and inventory decisions; Theorem 2 on estimation regret for both policies; and Proposition 8 on delayed detections and early false alarms for both policies. Every displayed clause and constant factor is retained.

What the formalization contributes

The claimed bounds distinguish the effect of learning a general disturbance distribution from learning a known exponential-family representation. Their shared benchmark includes inventory carryover and anticipation of changing demand. A complete verification would therefore address more than a static estimation problem or a stationary pricing policy.

This mission supplies concrete statistical objects, observable histories, inventory dynamics, estimator relations, and the actual regret sums. Definitions contain no unproved assertions. The theorem declarations are open statement drafts, not machine-checked proofs. Formalization also exposes source defects that require scrutiny. In particular, an admissible small horizon produces contradictory experimental prices, and the general maximum-likelihood result does not assume identifiability. The stated targets retain those defects so that a proof or a disproof addresses the source claim.

Where the difficulty lies

Estimation, reset times, and optimizer choices depend on the same observed data. Replacing the resulting sample indices by a fixed independent sample changes the problem. Arbitrary disturbance laws also prevent silently assuming density lower bounds, smooth quantile inverses, or uniformly positive link derivatives. The source's proof of pricing convergence contains a derivative-sign gap; no such derivative hypothesis is added to the statement.

Partial operations create a separate issue. A quasi-likelihood equation may lack a root, a likelihood may lack a maximizer, and an experimental inventory position may be infeasible. An arbitrary default action would define a different algorithm. The execution relation instead retains all prescribed equations and actual optimizer requirements.

Formalization scope and conventions

Prices and inventories remain continuous. Probability uses infinite independent primitive sequences, while actual rewards stop at $T$. The infinite sequence matters for the literal indexing formula in Lemma EC.2. General exponential families use an explicit dominating measure, permitting continuous and discrete distributions without imposing identifiability or a convex parameter set. Measurable optimizer selections retain ties. Expectations that appear in asserted guarantees carry integrability content, preventing a divergent integral from becoming Lean's default zero.

The probability bounds with random $M_t$ are read literally: the event probability is a scalar, and its displayed comparison with the random right side holds almost surely on the stated range. The reset times remain random inside the event. Noise-only probabilities integrate the noise sequence with the perishability sequence fixed, recomputing the history and estimates. The inventory lemma asserts existence of the level identified by both formulas, without adding uniqueness. It uses extended-real infima and suprema, preserving empty-sign-set failures. A concrete lower-bound optimum makes the strict-negative-derivative set empty even in a model with an interior FIA solution; this source counterexample is recorded alongside the other findings.

Equation (6) is read consistently with equations (1)–(2), retaining $g$. Proposition 8(b) uses the lower endpoint $n\widehat\tau_j^-+1$ appearing in the final decomposition. Both readings are declared per item and recorded as source findings. The source basis is published, but the supplied artifact is internally dated January 3, 2021 and contains SSRN footers; citations use its own pages, not invented journal pagination. Empirical extensions, age-dependent spoilage, censored-demand experiments, and externally cited lower bounds are outside this mission.

Selected references

• N. B. Keskin, Y. Li and J.-S. Song, Data-Driven Dynamic Pricing and Ordering with Perishable Inventory in a Changing Environment, Management Science, 2022. DOI. The supplied artifact contains the main text on PDF pages 1–32 and its electronic companion on PDF pages 33–54; the selected results occur on pages 12, 21–25, 33 and 40.

Continuous monitoring and the cost of waiting

An A/B experiment collects observations while a user decides whether the evidence is strong enough to act. A user may inspect the experiment repeatedly and stop when a result looks convincing. A test calibrated only for one sample size does not automatically retain its error guarantee under that behavior. A sequential test instead makes the stopping decision part of the statistical procedure. In the supplied Johari–Pekelis–Walsh preprint, the question goes beyond error control: how much sampling does a continuously monitored test require compared with every other test offering at least its power?

Different users can tolerate different delays. One may abandon an experiment after a modest number of observations; another may wait longer. The paper models these choices by a maximum sample count and a tolerated probability of false rejection. Its first-order efficiency claim concerns a single family of tests that can accommodate these choices without knowing them when the mixing distribution is selected. This mission addresses that claim, using the exact preprint version and theorem numbering stated below.

Observations, decisions, and mixtures

Let $X_1,X_2,\ldots$ be independent identically distributed real observations under each parameter law $P_\theta$. The natural parameter ranges over an arbitrary nonempty open interval $\Theta\subseteq\mathbb R$, and $\theta_0\in\Theta$ is the null. The alternatives are all other parameters in the interval. The source's exponential family has densities $f_\theta(x)=f_0(x)\exp(\theta x-\psi(\theta))$. The cumulant $\psi$ is twice differentiable, has strictly positive second derivative, and each observation law has finite fourth absolute moment. These are the standing assumptions of Section 5.2, page 18.

A decision rule consists of a positive integer stopping time $T$, possibly infinite, and a binary decision $\delta$. Decisions use only the observations available at stopping. Rejection means $\delta=1$; a test that never stops must not reject. The rule has no access to the unknown parameter or to independent randomization outside the observation filtration. Its Type I error is $P_{\theta_0}(\delta=1)$.

Fix a mixing distribution $H$ on $\Theta$ with continuous strictly positive density throughout the interval. For $S_n=n^{-1}\sum_{i=1}^nX_i$, define

$$\Lambda_n^H=\int_\Theta \exp\{n[(\theta-\theta_0)S_n-(\psi(\theta)-\psi(\theta_0))]\}\,dH(\theta).$$

The mixture sequential probability ratio test, or mSPRT, first stops at $T^H(\alpha)=\inf\{n\ge1:\Lambda_n^H\ge1/\alpha\}$ and rejects exactly when this time is finite. An empty crossing set gives infinity. A user with maximum count $M\ge1$ and tolerance $0<\alpha<1$ instead observes $\min(T^H(\alpha),M)$ samples and rejects when $T^H(\alpha)\le M$. Thus a crossing at the last allowed sample still rejects. These are equations (7)–(9) and Section 5.1.

Formalization targets

The sole supporting milestone is equation (10), page 19. For every fixed admissible $H$ and every fixed alternative $\theta$, set

$$I(\theta,\theta_0)=(\theta-\theta_0)\psi'(\theta) -(\psi(\theta)-\psi(\theta_0)).$$

The claim is

$$\frac{T^H(\alpha)}{\log(1/\alpha)}\longrightarrow I(\theta,\theta_0)^{-1} \quad\text{in probability and in }L^2(P_\theta),\qquad\alpha\downarrow0.$$

For the goal, the power profile of a bounded rule is $\nu_R(\theta)=P_\theta(\delta_R=1)$ and its relative run length is $\rho_R(\theta)=E_\theta[T_R]/M$. A feasible competitor stops by $M$ almost surely, has Type I error at most $\alpha$, and has power at least the truncated mSPRT's power at every alternative. The competitor need not belong to a nested family of tests. Definition 3, page 21, defines

$$\phi(M,\alpha)=\inf_{R\ \mathrm{feasible}}\inf_{\theta\in\Theta\setminus\{\theta_0\}} \frac{\rho_R(\theta)}{\rho_H(\theta;\alpha,M)}.$$

The goal is the complete Theorem 2, page 21: if $\psi''$ is absolutely continuous on its parameter interval and finite on an open neighborhood of $\theta_0$, then, for every fixed admissible $H$,

$$\phi(M,\alpha)\longrightarrow1\quad\text{as }\alpha\to0,\quad M\to\infty, \quad M=O(\log(1/\alpha)).$$

The constant is exactly one. Both infima stay inside the limit. All qualifying paths are included, even when $M/\log(1/\alpha)$ tends to zero.

What the comparison would establish

The efficiency claim compares sample use with an entire class of decision rules, while requiring that competitors match power at every alternative. It therefore addresses a stronger question than the runtime of one test at one parameter. The mixture is fixed before the user's asymptotic choices; the first-order claim does not optimize a new mixture at each tolerance.

The source presents this as a theorem. The present formalization supplies open Lean statements, not completed proofs. It also records two gaps in the printed argument and a support ambiguity in its likelihood notation. Formal work can determine whether the complete printed target is provable or admits a counterexample. Those findings do not replace the goal with a repaired or restricted claim.

Why pointwise limits do not settle efficiency

Convergence of the runtime at each fixed alternative does not imply convergence after taking an infimum over all alternatives and all feasible rules. Alternatives can approach the null or move toward the boundary as the tolerance changes. The printed proof on pages 42–43 obtains a comparison at a selected alternative, which alone cannot lower-bound the full infimum. It also substitutes a parameter that need not approach zero into an expansion stated as the parameter tends to zero. These are identified proof gaps, not asserted counterexamples to the statistical theorem.

Formalization scope

The model reuses the published scalar exponential-family definition with scale one and zero base log density. An arbitrary reference measure is allowed; choosing $f_0(x)\,dx$ recovers every density family in the source. Observations may live on any measurable probability space, while the history sigma algebras are exactly those generated by the observed coordinates. Coordinate zero represents $X_1$.

Stopping times use extended natural numbers. Nonnegative expectations and both infima use extended nonnegative reals. Infinite stopping times are never replaced by zero. At valid finite horizons, positive sample counts give positive finite denominators; the mSPRT's error control supplies a feasible competitor. These facts must follow from the definitions rather than enter as assumptions. The milestone includes square integrability and almost-sure finiteness in its conclusion. The goal uses every valid sequence to express the joint limit.

Equation (7) is read as the exponential likelihood ratio after cancellation of the carrier density. This agrees with its quotient wherever defined. A carrier with disconnected support can give a sample mean where the printed quotient is $0/0$; that issue is recorded explicitly. No everywhere-positive carrier assumption is added. Definitions of binary decisions, positive-density mixtures, natural histories, and efficiency support further sequential-testing work.

Selected references

• R. Johari, L. Pekelis, and D. Walsh, Always Valid Inference: Continuous Monitoring of A/B Tests, arXiv preprint, 2019, arXiv:1512.04922v3, Sections 3 and 5.1–5.3, equation (10), Definition 3, Theorem 2, and Appendix A. All source numbers in this mission refer exclusively to this pinned version.

Motivation: removing time-discretization bias

A Monte Carlo price estimate averages discounted payoffs over simulated scenarios. Its statistical error can be assessed from the variation of those payoffs. When a continuous-time stochastic model is replaced by a finite time grid, a second error enters: the simulated distribution differs from the model distribution. Increasing the number of scenarios does not remove that bias at a fixed grid. Broadie and Kaya address this problem for stochastic volatility by constructing samples of terminal stock price and variance from their joint law. Their published paper develops the Heston construction first and then considers jump extensions and pricing applications. This mission concerns the complete Heston construction of §3 and its unbiased-pricing consequence.

Setting: stock price and square-root variance

The Heston model describes a stock price $S_q$ and its instantaneous variance $V_q$. Under the risk-neutral probability measure they solve

$$dS_q=rS_q\,dq+\sqrt{V_q}S_q\bigl(\rho\,dW_q^{(1)}+\sqrt{1-\rho^2}\,dW_q^{(2)}\bigr),$$ $$dV_q=\kappa(\theta-V_q)\,dq+\sigma_v\sqrt{V_q}\,dW_q^{(1)}.$$

Here $W^{(1)}$ and $W^{(2)}$ are independent standard Brownian motions. The real number $r$ is the risk-neutral drift, $\kappa>0$ is the speed of mean reversion, $\theta>0$ is the long-run variance, and $\sigma_v>0$ is the volatility of variance. The correlation $\rho$ ranges over the closed interval $[-1,1]$. These are the dynamics in (1)–(2), p. 218.

Fix arbitrary deterministic times $0\le u<t$, write $\Delta=t-u$, and start at $(s,v)$ with $s>0$ and $v\ge0$. The processes are continuous and adapted, with stochastic integrals interpreted locally in the Itô sense. The integrated variance is $A=\int_u^tV_q\,dq$. The dimension parameter $d=4\kappa\theta/\sigma_v^2$ is any positive real number. The regime in which variance can reach zero remains in scope; the condition $2\kappa\theta\ge\sigma_v^2$ is not imposed.

Formalization targets

The main target is equality of the joint laws of the original SDE and the paper's explicit ideal sampler:

$$\mathcal L(\widehat S,\widehat V)=\mathcal L(S_t,V_t).$$

For random starting states, this is an almost-everywhere equality of conditional probability measures given $(S_u,V_u)$. The sampler is defined independently: it draws a scaled real-degree noncentral chi-square variance, uses the explicit continued characteristic function and Fourier inverse CDF for integrated variance conditional on that sampled variance, recovers the first Brownian integral algebraically, and uses an independent standard Gaussian for the stock draw. This is the four-step algorithm and its completion in §3.3.

For any measurable payoff $f$ on the two terminal coordinates, put $g=e^{-r\Delta}f$ and $P_f=E[g(S_t,V_t)]$. Independent sampler repetitions give the ordinary empirical average $\widehat P_N$. Whenever $g$ is absolutely integrable, the target includes

$$E[\widehat P_N]=P_f\qquad(N\ge1).$$

For nonnegative payoffs, expectation equality is also stated with possibly infinite values. If $g$ has a finite second moment, write $\sigma_f^2=E[(g-P_f)^2]$. Then

$$\operatorname{MSE}(\widehat P_N)=\frac{\sigma_f^2}{N},\qquad \operatorname{RMSE}(\widehat P_N)=\frac{\sigma_f}{\sqrt N}.$$

Under the fixed per-path cost convention $s_{\rm budget}=cN$, $c>0$, the latter equals $\sigma_f\sqrt c/\sqrt{s_{\rm budget}}$. The asymptotic rate is $O(s_{\rm budget}^{-1/2})$, with the explicit coefficient fixed independently of sample count. This is the §1 cost convention and p. 219 standard-error identity. It is not a claim about the bit complexity of special-function evaluation.

Seven source displays supply the milestones: the stock exponential representation (6); the scaled noncentral chi-square transition law (8)–(9); the squared Bessel bridge transform (39); the square-root bridge Laplace transform (40); its characteristic-function counterpart (13); both Fourier inversion equalities (14); and Brownian-integral recovery (23). Each retains its coefficients and full parameter domain.

Significance: exact laws and statistical error

Equality of joint laws makes the pricing result applicable to payoffs depending on both terminal stock and terminal variance, a scope expressly described in §8. It also separates the assumptions needed for different conclusions: exact simulation is distributional, unbiased real-valued pricing needs an absolute first moment, and the RMS formula needs a second moment. These distinctions matter for unbounded payoffs.

The paper establishes these results mathematically. This mission supplies open Lean statements and concrete definitions for formalizing them; it does not claim that their proofs have already been checked. The reusable contributions include real-degree noncentral chi-square sampling, continuous endpoint bridge semantics, and a complex Bessel ratio that retains its branch and boundary conventions. The local Itô-integral foundation is reused from a published definition.

Difficulty: dependence, continuation, and boundary values

Knowing the marginal laws of terminal variance and integrated variance is insufficient. They are dependent, and the stock formula uses that dependence. Replacing the bridge draw by an independent marginal draw changes the joint law. Similarly, the conditional normal expression for the stock does not by itself prove that the inputs to that expression have the required distribution.

The characteristic expression (13) contains a modified Bessel function at a complex argument. The source explicitly requires continuation between branches in (22). Principal-branch evaluation alone can introduce a discontinuity. Zero variance endpoints create another difficulty: the raw numerator and denominator can both vanish or diverge, while their ratio has a meaningful continuous extension. Finally, Fourier inversion must establish a genuine continuous CDF and a valid inverse-transform draw; these properties cannot be supplied as premises.

Formalization scope

The original processes are defined by SDE integral equations on a usual filtered probability space. The published local Itô relation uses bounded predictable approximations and convergence in probability, without requiring global expected squared energy. The generic square-root processes are separate from the paper-specific multiplicative stock model. Neither definition contains a terminal distribution or sampler-correctness field.

Conditional laws at random states use regular conditional distributions almost everywhere. For deterministic endpoints, bridge laws are specified by weak limits of conditioning on shrinking positive-width terminal observation windows. Their existence is asserted in the bridge theorems. The Bessel quotient cancels the common endpoint power through the entire factor $H_\nu$ from (21); the continued logarithm tracks the frequency path. Both infinite Fourier integrals are represented by limits of truncated integrals, and quantile well-definedness is part of the inversion conclusion.

The sampler uses ideal real and complex operations. The finite trapezoidal sum and numerical tolerance discussion in §3.2 describe an approximation to that ideal construction. They are not an exact finite-precision implementation. Jump-model extensions, conditional variance reduction, Greeks, and forward-start pricing are separate results outside this mission's selected goal. Proof contributions can develop the stochastic, analytic, or probability-measure foundations without changing the selected statements or their domains.

Selected references

• Mark Broadie and Özgür Kaya, Exact Simulation of Stochastic Volatility and Other Affine Jump Diffusion Processes, Operations Research 54(2), 217–231, 2006. Published article. The mission uses this version throughout, especially §§2.1 and 3, the Appendix, and the statistical conventions in §§1–2.2.

Learning prices while selling limited inventory

A retailer must learn demand while selling a fixed stock over a finite season. A high price preserves inventory but may leave profitable sales unrealized. A low price can exhaust stock before later customers arrive. Learning is harder when some customers behave unlike the population whose demand the retailer wants to learn. Those customers can arrive in a concentrated block and can adapt to what has already happened. The problem studied by Chen and Wang asks for pricing rules whose revenue loss remains controlled without knowing the number of these outliers or whether inventory will bind at the unconstrained optimal price.

This mission concerns the paper's modular general-inventory result. Its inputs are two pricing policies with guarantees in the two opposite inventory regimes. Its target is the guarantee claimed for the particular randomized meta-policy that combines them. The input guarantees remain assumptions, rather than being replaced by guarantees for a specially chosen pair of implementations.

A continuous-price model with adaptive outliers

There are T selling periods and real initial inventory $x_0T$, where $0<x_0\le1$. Prices lie in a compact nonnegative interval $[\underline p,\overline p]$. The unknown typical demand curve $f_0$ decreases strictly from 1 to 0 across that interval. The curve and its inverse satisfy the two-sided Lipschitz assumptions printed in the paper. The demand-coordinate revenue, $r(d)=df_0^{-1}(d)$, is twice continuously differentiable on $(0,1)$, with $0<\sigma^2\le-r''(d)\le M^2$.

An adaptive adversary chooses whether each customer is an outlier and, if so, a measurable alternative demand curve into $[0,1]$. These choices can use the full past of prices, sales, demand curves and outlier indicators. They precede the current price decision. The seller sees only earlier prices and sales, together with its own private randomness. The total number of outliers is at most $\varepsilon T$ almost surely for every policy. A fixed positive α satisfies $\varepsilon\le T^{-\alpha}$. The seller does not receive ε, α, the typical curve, or the true inventory regime.

At a chosen price, sales are demand plus noise censored by the remaining physical stock. Sales belong to $[0,1]$, and revenue is price times actual sales. Noise has mean zero conditional on the current price, as stated in §3; independence across periods and mean zero conditional on the entire history are not assumed.

The clearance price is $p^c=f_0^{-1}(x_0)$, and the unconstrained revenue optimum $p^o$ maximizes $pf_0(p)$ over the continuous interval. The typical-demand fluid benchmark is

$$r^*=\max_{p\in[\underline p,\overline p]}p\min\{f_0(p),x_0\}.$$

Regret is $Tr^*$ minus expected cumulative actual revenue. The expectation includes both seller randomization and customer randomness. The model and inventory rate stay fixed as T grows.

Formalization targets

The supporting targets, in proof-use order, are the e-companion's Lemma EC.4, its Lemma EC.3, main-text Lemma 5, and Corollary EC.1. The first is the uniform martingale inequality

$$\Pr\{\exists n\ge1:S_n\ge a,\ V_n^2\le y\}\le\exp[-a^2/(2(y+ca))].$$

The next bounds the error in a sampled fixed-price demand average, using the corruption count within the selected periods and positive stock at their beginnings. Lemma 5 gives both simultaneous exploration-estimate errors, with every printed constant and its full $H_Z$ expression. Corollary EC.1 asserts

$$|\widehat p^c-p^c|+|\widehat p^o-p^o|\le0.2|p^o-p^c|$$

with probability $1-O(T^{-2})$ under its printed parameter and polynomial-threshold conditions.

The goal is Theorem 4, covering both strict regimes $p^c<p^o$ and $p^c>p^o$. If the two supplied policies have their respective uniform $\widetilde O(\varepsilon T+\sqrt{T''})$ regret guarantees, then the specified Algorithm 5 satisfies

$$R_{T,\varepsilon T}=\widetilde O(\varepsilon T+\sqrt T)$$

for sufficiently large T. The absolute subroutine corruption budget is εT. The excluded equality case stays excluded. The polynomial parameter dependence and logarithmic factors are represented with constants and degrees chosen before horizons, contamination levels and environments.

What the formalization contributes

The target transfers guarantees for policies that know their applicable inventory regime into a guarantee for the paper's specified combination. Its operational definitions separate reusable randomized observed-history policies from the pricing model, real inventory dynamics, exploration estimator and meta-policy. This makes the meaning of actual revenue and the seller's information available for inspection independently of any proof.

The source presents these results with proofs, but this mission supplies open Lean statements rather than completed machine-checked proofs. Source findings are retained separately: the printed exploration normalization admits a counterexample to Lemma 5, and the stated price-conditioned noise assumption admits a counterexample to Lemma EC.3. Those claims remain exactly the targets to prove or disprove; they are not silently replaced by corrected versions. Corollary EC.1 also retains a printed maximum whose use in the proof needs scrutiny.

Why the claim requires care

Exploration competes with revenue collection for the same physical inventory. A successful estimate obtained after stock has been depleted cannot restore the lost opportunity. Outliers can cluster early, and the two input policies need different conditions to make their guarantees applicable. Neither the regime estimates nor successful exploration can be assumed in a faithful statement. The distinction between conditioning noise on price and conditioning it on the whole past is also consequential: the latter would impose a stronger statistical model than the paper prints.

Formalization scope and conventions

All prices, sales and stock quantities are real. Time is indexed by elapsed periods starting at zero. The general policy interface takes only public initialization data, private randomness and observed price/sales history. Environment randomness ranges over arbitrary measurable spaces and is independent of the private tape; its response may depend on the current price. The almost-sure budget is required for every admissible policy. Measurability and integrability make expectations meaningful, without bounding uncensored noise.

Algorithm 4 uses the endpoint-inclusive grid and the printed estimate $N_3\widehat d(i)/T_0$, with $T_0=\lceil\sqrt T\rceil$. Ties use the lowest index. Pricing outside a selected exploration set uses a separate private tape, preserving fresh exploration draws. Algorithm 5 samples a private epoch schedule, uses its realized cardinality for the grid, and interleaves exploration with the selected input policy. The prior epoch's observations determine the next branch. Each subroutine receives the nominal epoch horizon and nominal stock allocation; its history advances only on its assigned periods. The nominal quota is checked between selling periods to determine subsequent prices; individual sales are censored by actual global stock, which is shared and never reset.

The source omits zero/singleton-grid behavior despite giving those events positive probability. The explicit completion returns the lower endpoint for both estimates and uses the lower price on a singleton grid. No event is excluded from the goal. Theorems 1–3 and the independent lower-bound Theorem 5 are outside this mission's dependency scope. The meta-policy's regret guarantee occurs only in the goal conclusion, never in its definition or an algorithm-validity assumption.

Selected references

• Xi Chen and Yining Wang, Robust Dynamic Pricing with Demand Learning in the Presence of Outlier Customers, Operations Research, DOI 10.1287/opre.2022.2280. The catalog uses the 2020 paper identifier; citations here use the supplied manuscript's pp. 10–13 and 29–32, not independently verified journal pagination.
• Xi Chen and Yining Wang, e-companion to Robust Dynamic Pricing with Demand Learning, accompanying the same DOI, publisher file opre.2022.2280.sm1.pdf, ec9–ec10 and ec13–ec17. Both pinned local PDFs belong to this single citation family.

Motivation

Retailers sometimes offer a discount on a game only after a customer buys a console. Such add-on discounts let the customer choose individual additional products while the retailer controls both the original prices and the conditional offers. A retailer with limited transaction history must learn purchase probabilities while choosing these prices. Offering discounts on only a limited number of products adds a selection decision to the pricing problem. Simchi-Levi, Sun and Zhang study this joint learning and optimization problem in arXiv:2005.00947v1. This mission concerns their UCB-Add-On regret theorem and the five supporting lemmas used in its argument.

Setting

A retailer has core products, numbered by a positive integer $N$, and supportive products, numbered by a positive integer $M$. Core prices belong to a finite nonempty menu $\Omega_c$. Original supportive prices belong to $\Omega_s$, and discounted supportive prices belong to $\Omega_a$. All prices are nonnegative real numbers. There is no rational-grid assumption. The nonnegative integer $S$ limits the number of discounted supportive products; it may be zero or exceed $M$.

A policy $\pi$ specifies a core price $p_n$ for each core product, an original price $s_m$ and discount price $a_m$ for each supportive product, and a Boolean selection $I_m$. Feasibility means $\sum_m I_m\le S$ and $a_m<s_m$ for every supportive product, including those not selected. The operational problem has at least one feasible policy.

The demand tables are arbitrary fixed functions with values in $[0,1]$. The mean primary purchases are $\alpha_n(p_n)$ for core products and $\alpha_{N+m}(s_m)$ for supportive products. Each core purchase creates an opportunity to buy each supportive product, with mean $\beta'_m(a_m)$ when selected and $\beta_m(s_m)$ otherwise. Fresh primary purchases are independent Bernoulli observations; conditional on those purchases, the add-on opportunities receive independent Bernoulli observations. A period can contain any number of core purchases from zero to $N$. There is no inventory depletion or assumption that a customer selects at most one core product.

The expected revenue is

$$R(\pi)=\sum_n\alpha_n(p_n)p_n+\sum_m\alpha_{N+m}(s_m)s_m+ \left(\sum_n\alpha_n(p_n)\right)\sum_m\left[I_m\beta'_m(a_m)a_m+(1-I_m)\beta_m(s_m)s_m\right].$$

The benchmark $R^*$ is the attained maximum over the feasible policies in equation (1). The same polynomial evaluates an algorithm output even if the printed procedure produces a tuple that fails the unconditional discount-price constraint.

Algorithm 1 optimizes supportive revenue at demand grid points, ranks the benefit of offering each discount, rounds core demand to the nearest multiple of $1/K$, and recovers maximizing policies from a backward dynamic program. Algorithm 2 estimates all four parameter families. Primary counters count periods; add-on counters count core-purchase opportunities. At episode start $t$, each positive-count upper confidence bound is $\min(1,\bar\alpha+\sqrt{2\log(t)/c})$, with the corresponding empirical mean for each family. Algorithm 1 receives these estimates and $K=\lceil\sqrt t/\varepsilon\rceil$. Its output is held until an associated counter doubles, including overshoots.

Formalization targets

Define $\widehat p=\max(\Omega_c\cup\Omega_s)$ and $U=\max(|\Omega_c|,|\Omega_s|,|\Omega_a|)$. Let $\lambda$ be the minimum probability of nonzero total primary demand over feasible policies, including primary supportive demand. Regret is the expectation of $\sum_{t=1}^T(R^*-R(\Pi_t))$ under the algorithm's own trajectory law.

The goal is Theorem 2, page 16, equation (7):

$$\operatorname{Regret}(T)=O\!\left(NM\widehat p\left[\lambda^{-1}\sqrt{UT\log T}+\varepsilon\sqrt T\right]\right).$$

One positive absolute multiplier precedes the instance and $\varepsilon$. The eventual horizon threshold may depend on the instance and $\varepsilon$, but precedes every controller and tie choice. At $\lambda=0$ the upper bound is infinite.

The milestones retain the source's use order: Lemma 4 bounds expected episode length by its starting time; Lemma 5 bounds total bad-event episode regret by a horizon-independent constant; Lemma 1 asserts the exact supportive Lipschitz constant $M\widehat p$; Lemma 3 asserts actual-revenue approximation error at most $\widehat p MN/K$; Lemma 6 bounds good-event episode regret by a constant times both terms of the displayed rate. The independent offline FPTAS theorem and lower-bound remark are outside this mission.

Significance

The regret claim quantifies the cumulative cost of learning demand while computing approximate pricing decisions. Its displayed dependence distinguishes the number of products, the number of candidate prices, the price scale and the approximation input. Keeping these factors explicit prevents an instance-dependent asymptotic constant from hiding the central claim of Theorem 2.

The formalization supplies concrete declarations for the pricing model, both algorithms, the observation law and the source's claims. The six theorem declarations are statements awaiting proofs or disproofs. Compiling them does not establish the printed results. In particular, the literal supportive subproblem has a counterexample to its claimed Lipschitz constant, and other source discrepancies require careful separation from the intended analysis.

Difficulty

Feedback for supportive add-on demand arrives only when a core purchase creates an opportunity. Those counts can remain zero even when total primary demand is always positive. Episode lengths and the histories at which confidence events are tested are random. Replacing this feedback by a policy-level reward observation changes the learning problem.

The source also leaves initialization and zero-start doubling unspecified. Its displayed bad event uses $2\log(t)/c$ without the square root in the algorithm. Equation (3) reverses the strict price inequality used in equation (1), while Algorithm 1's ordinary branch can select an original price with no smaller discount available. These issues are retained explicitly; a corrected algorithm or corrected lemma would be a separate result. In particular, completing an unseen profitable core price with UCB zero can leave it unexplored forever and give linear regret. The universal-completion targets include this case; the initialization insight records the explicit two-price example.

Formalization scope

Finite menus use injective real-valued labels and products use finite index types. Demand values zero and one are included. All rounding and maximizing ties are admitted. The generic probability-mass object is Mathlib's PMF; the paper-specific controller uses distributions on finite policy tuples and post-observation stopping probabilities. Recursively multiplied finite kernels define every finite-horizon expectation. No concentration, optimism, approximation error or regret inequality is included in a run condition.

Undefined zero-count UCB branches range over all causal values in $[0,1]$. Undefined zero-start stopping branches range over all causal almost surely finite positive completions, while every defined positive-count doubling stop is enforced. These are declared generalizations, not a favorable initialization convention. The bad event likewise includes every history-determined Boolean completion at zero counts. Its positive-count radius remains literal. Event contributions use indicator weighting at the actual episode-start history and truncate the final episode; full conditional episode length uses an extended nonnegative tail sum.

The printed supportive maximum has its own feasible set and nonemptiness condition. Operational benchmark feasibility is separate. This separation keeps the reversed-price counterexample expressible without imposing it on the online model. The concrete definitions support future proof and disproof work without assuming any of the target bounds.

Selected references

• David Simchi-Levi, Rui Sun and Huanan Zhang, Online Learning and Optimization for Revenue Management Problems with Add-on Discounts, arXiv preprint, 2020, arXiv:2005.00947v1, Sections 2–4, Algorithms 1–2, Lemmas 1, 3–6 and Theorem 2. PDF and printed pages agree for pages 1–33.

Learning while acting

A seller choosing prices may learn about demand from purchases while earning revenue from those same purchases. The hidden customer characteristic can range continuously, even when there are only a few prices and observations. A policy must therefore trade off present reward and information that affects later decisions. Describing every possible belief about a continuous parameter makes a direct dynamic program difficult to represent.

Hao Zhang's Dynamic Learning and Decision Making via Basis Weight Vectors studies a different representation: the reward of a continuation policy as a function of the hidden parameter. The exact result in Section 4.1 states that polynomial primitives permit the relevant family of these functions to be recovered through operations on finite coefficient vectors. This mission concerns that exact result, including its whole efficient frontier at every period.

Operational setting and the two frontiers

A parameter $\theta\in\Theta=[0,1]$ is selected before a horizon of $T$ decision periods and stays fixed. At each period an agent chooses an action from a finite nonempty set $A$ and receives a signal from a finite nonempty set $S$. Conditional on action $a$ and the parameter, signal $s$ has probability $p(s\mid\theta,a)$. These probabilities are nonnegative and sum to one. The associated reward $r(\theta,a,s)$ is real and may be unobserved. The discount factor satisfies $0<\delta\le1$.

A continuation policy is a finite tree whose root chooses an action and whose child is selected by the next signal. Its choices never observe $\theta$. Its continuation-value function $u(\theta)$ is its expected discounted reward conditional on that fixed parameter. A terminal continuation function supplies the boundary value. A finite efficient family of terminal functions is also permitted, covering the soft termination described in assumption (A2).

The positive-normal extreme frontier, written $\operatorname{PNEP}$, retains strictly exposed members of a finite set. For vectors in $\mathbb R^{d+1}$, an exposing normal $\rho$ has nonnegative coordinates summing to one. It must give its chosen member a strictly larger inner product than every distinct competitor. For functions on $[0,1]$, normals are all nonnegative square-integrable densities $\pi$ with integral one, and the comparison is $\int_0^1\pi(\theta)u(\theta)\,d\theta$. The two spaces have different families of normals.

The basis-weight representation uses monomials $\phi_i(\theta)=\theta^i$. A weight $w=(w_0,\ldots,w_d)$ represents $\Phi w=\sum_iw_i\phi_i$. Coefficients may be negative, even for a nonnegative probability function. Weight addition uses zero padding, and $a\otimes b$ is ordinary coefficient convolution. Assumption (A1) supplies weights for every probability and reward function. Assumption (A2) supplies weights for every terminal frontier member.

Exact formalization targets

The three supporting statements are Lemma 1, Corollary 1 and Lemma 3. The first retains both algebraic identities, including unequal vector lengths:

$$\Phi a+\Phi b=\Phi(a+b),\qquad (\Phi a)\odot(\Phi b)=\Phi(a\otimes b).$$

The second identifies expected-reward weights:

$$\bar r(a)=\Phi w_{\bar r}(a),\qquad w_{\bar r}(a)=\sum_{s\in S}w_p(a,s)\otimes w_r(a,s).$$

Here $\bar r(a)(\theta)=\sum_s p(s\mid\theta,a)r(\theta,a,s)$.

For a finite weight set $W$ and a nonnegative basis family, Lemma 3 says that every member of $\operatorname{PNEP}(\Phi W)$ is represented by a member of $\operatorname{PNEP}(W)$, and

$$\operatorname{PNEP}(\Phi W)=\operatorname{PNEP}(\Phi\operatorname{PNEP}(W)).$$

The goal is Theorem 1. Initialize $W_{T+1}^*=\{w(u):u\in U_{T+1}^*\}$. For every $t=1,\ldots,T$ and every $a\in A$, compute

$$W_t^*=\operatorname{PNEP}\left(\bigcup_{a\in A}W_t^*(a)\right),$$ $$W_t^*(a)=\operatorname{PNEP}\left(\left\{w_{\bar r}(a)+\delta\sum_{s\in S}w_p(a,s)\otimes w_{t+1}(s):w_{t+1}(s)\in W_{t+1}^*\ \forall s\right\}\right).$$

Then the independently defined function recursion of Eqs. (7)–(9) is recovered exactly:

$$U_t^*=\operatorname{PNEP}(\{\Phi w:w\in W_t^*\}).$$

Every period and action is retained. The terminal function family and terminal weight family are the prescribed boundary data. There is no approximation constant or degree truncation.

What the exact representation provides

The result replaces the manipulation of continuation functions with finite coefficient arithmetic while preserving the complete frontier relevant to density normals. It concerns an entire family of policies and priors, rather than a value for a single selected prior. The polynomial degree and number of candidate vectors can still grow; exact representability does not assert inexpensive computation. The source's approximation methods and empirical comparisons are separate from this claim (Zhang, Sections 4.3–5.6).

Formalization makes the two exposure notions, the information restriction on policies, and the terminal boundary explicit. The theorem declarations are proof targets; their compilation checks their types and definitions, not the validity of the asserted results. A completed development would provide checked algebraic and geometric statements for this representation.

Why the frontier comparison matters

Exact coefficient arithmetic alone does not establish the theorem. A coefficient vector can be exposed by a simplex normal while its evaluated function is dominated on the parameter interval. The paper illustrates this with the weights representing $1$, $\theta$ and $\theta^2$: every coordinate vector is exposed in coefficient space, but only the constant function survives function-space exposure. Consequently, the outer function-space PNEP in the recovery equality is essential (Zhang, p. 17, footnote 5).

The operational function recursion and the weight recursion are defined independently. Their agreement is a conclusion. Finite observations do not turn the hidden parameter into a finite state space, and probability nonnegativity does not imply coefficient nonnegativity.

Formalization scope and conventions

The interval is a subtype of the reals with its Lebesgue measure. Function equality is pointwise on that interval. The weight type is the real polynomial type, which represents finitely supported coefficients modulo trailing zeros. Finite normalized normals are tested at a common degree bound for each set; the bound is unrestricted. Polynomial multiplication supplies convolution. All primitive and generated functions are square integrable, so the density comparisons use integrable products.

Natural-number indices count remaining decisions: zero is terminal, and $n+1$ is computed from $n$. For a horizon $T$, the source period is $t=T-n$ at the update indexed by $n<T$. Lemma 3 permits arbitrary nonnegative L2 basis families, with independence interpreted in the source Hilbert space. The definition layer also includes policy trees, operational probabilities and rewards, terminal representations and both recursions.

Definition 4's component count is read as $\max(d_a,d_b)+1$, consistent with its zero-based indexing and its preceding example. This reading is recorded in insight I1 and in theorem differences. Gaussian, exponential, multivariate and spline extensions, numerical performance, and proofs of the approximation methods are outside this mission. Insights I2 and I3 retain the source findings about excluded appendices.

Selected references

• Hao Zhang, Dynamic Learning and Decision Making via Basis Weight Vectors, Operations Research, 2022. DOI 10.1287/opre.2021.2240. This mission uses the supplied published-basis artifact: model and definitions on PDF/printed pp. 7–16; Lemma 3 and Theorem 1 on p. 17; proofs on PDF pp. 52–53, EC pp. 8–9. The supplied PDF retains manuscript pagination and SSRN footers.