All missions

Motivation

Multistage stochastic optimization chooses a sequence of decisions while information arrives over time. A decision at time $t$ may depend on the observations available by then, but not on later outcomes. That information restriction, called nonanticipativity, links decisions across scenarios. Dual variables for it are useful because they express how an information constraint affects the optimum and because they lead to conditions that can be checked scenario by scenario. The paper studies this question for convex objectives on spaces of random variables broad enough to include strategies without integrability restrictions. Earlier duality models often worked on a smaller space or required multipliers in a full topological dual whose elements are not always random variables. Pennanen and Perkkiö, 2022 ask when the dual optimum can instead be attained by random-variable multipliers.

The distinction matters even if the two dual problems have equal values. A strong dual solution can include a singular functional that cannot be expressed as integration against a random variable. A numerical or economic interpretation of a dual multiplier usually needs the latter representation. The paper's result therefore includes both equality of values and actual attainment in the ordinary dual. Its final optimality condition concerns the original problem over all adapted measurable strategies, not merely the locally convex space used to construct the dual.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space with a finite filtration $(\mathcal F_t)_{t=0}^{T}$. A process $x=(x_t)$ is adapted when each $x_t$ is measurable using information at time $t$. Write $\mathcal N$ for the linear space of adapted processes. The objective is the integral $Ef(x,u)=\int f(x(\omega),u(\omega),\omega)\,dP(\omega)$ of a convex normal integrand $f$: each scenario has a closed convex extended-real objective, and the epigraphs vary measurably with the scenario. The paper assigns $+\infty$ to the integral when the positive part is not integrable. A fixed random parameter $\bar u$ gives the original problem $(SP)$: minimize $Ef(x,\bar u)$ over $x\in\mathcal N$. These conventions and the model are stated on pages 1–3 of the pinned preprint.

For duality the paper uses locally convex spaces $\mathcal X$ and $\mathcal U$ of random variables, with $\bar u\in\mathcal U$ and $\mathcal X_a=\mathcal X\cap\mathcal N$. The associated problem $(SP_{\mathcal X})$ minimizes $Ef(x,\bar u)$ over $\mathcal X_a$. Its value function $\varphi(z,u)$ allows the nonanticipativity constraint to be shifted by $z$. The spaces $\mathcal X$ and $\mathcal U$ are solid and decomposable, and they pair by expected dot product with random-variable spaces $\mathcal V$ and $\mathcal Y$. Strong Fréchet topologies give larger topological duals $\mathcal X^*$ and $\mathcal U^*$; each splits uniquely into a random-variable part and a singular part.

The ordinary dual $(D)$ maximizes $\langle\bar u,y\rangle-Ef^*(p,y)$ over $p\in\mathcal X_a^\perp$ and $y\in\mathcal Y$. Here $Ef^*$ integrates the pointwise conjugate $f^*$, while $\mathcal X_a^\perp$ consists of members of $\mathcal V$ annihilating every adapted element of $\mathcal X$. The strong dual $(D_s)$ maximizes $\langle\bar u,y\rangle-\varphi^*(p,y)$ over the full topological duals. Their distinction is the central object of the mission.

Formalization targets

Dual values and attainment

The goal is Theorem 27 on page 20. Under Assumption 23 and closed linearity of $\operatorname{pos}(\operatorname{dom}\varphi-(0,\bar u))$, it gives

$$\inf(SP)=\inf(SP_{\mathcal X})=\sup(D),$$

and an attaining pair in $(D)$. Assumption 23 has two parts: the positive hull of $\operatorname{dom}_{u}Ef-\bar u$ is a closed linear space, and a feasible point can be replaced by another feasible point whose coordinates through time $t$ equal their conditional expectations. The paper's displayed formula repeats “$(SP)$” in the second position; the distinct restricted problem defined on page 2 supplies the reading used here.

Scenario-wise optimality

For a feasible adapted strategy $x$ with finite objective, the goal also identifies primal optimality with a dual feasible pair satisfying

$$(p(\omega),y(\omega))\in\partial f(x(\omega),\bar u(\omega),\omega) \quad\text{for almost every }\omega.$$

The supporting targets are Lemma 13, which separates the regular and singular pieces of an approximate integral-functional subgradient; Theorem 18, which establishes strong dual attainment; Lemma 24, which controls a support function after conditional expectation; Theorem 25, which supplies ordinary dual variables; and Theorem 26, which compares the two dual values and their attainment. Theorem 14's conjugate and subgradient formulas are included as a supporting theorem item, with its lower-semicontinuity equivalence left outside this mission.

Significance

The equality between $(SP)$ and $(SP_{\mathcal X})$ says that constructing duality in the locally convex space has not changed the value of the unrestricted adapted problem. Equality with $(D)$ and attainment then provide actual random-variable multipliers rather than only a supremum or singular dual solutions. The pointwise subgradient condition converts an optimality claim about a coupled stochastic program into conditions on the scenario integrand. These are the consequences asserted in the source's Theorem 27.

The result is proved in the source, but this mission's Lean statements are open proof obligations. A completed development would add a reusable treatment of convex integral functionals with extended-real values, singular dual decompositions, adapted almost-everywhere classes and support functions under conditional expectation. The definitions are shared across the goal and milestones so that a proof of one result addresses the same objects used by the others.

Difficulty

Strong duality alone does not supply the ordinary dual variables. The strong topological duals may contain singular functionals, so an optimizer of $(D_s)$ need not lie in $\mathcal V\times\mathcal Y$. The source must show that under Assumption 23 those singular components can be removed without worsening the dual objective. Conditional expectation interacts with the time structure of a process and the domain of $Ef$; this is where a direct appeal to an abstract convex-duality theorem stops short of Theorem 27. Separately, the original primal problem permits adapted strategies outside $\mathcal X$, so its value cannot be identified with $(SP_{\mathcal X})$ by definition.

Formalization scope

Lean represents random variables as classes modulo almost-everywhere equality. Each Euclidean process block is flattened to coordinates indexed by a finite type, with a time stamp recording its filtration stage. Adaptedness means that every coordinate has an $\mathcal F_t$-measurable representative. Strong topologies live on the types $\mathcal X$ and $\mathcal U$ embedded into those classes; the regular dual partners remain submodules of random-variable classes. The setting explicitly states their Fréchet properties, solidity, decomposability, separating pairings, integrability of pairing products, and unique regular–singular dual decompositions. Continuity of each regular pairing expresses the source's Mackey-strength condition. Conditional expectation closure is a separate section-four hypothesis.

Primal and dual values, conjugates and support functions take values in the extended reals. The ordinary dual uses the integral of the pointwise conjugate and ranges over $\mathcal X_a^\perp\times\mathcal Y$; $(SP)$ ranges over all adapted measurable classes. Thus neither problem can become true merely by restricting to $\mathcal X_a$ or redefining the ordinary objective with $\varphi^*$. The positive-part integral convention uses the previously published expectation definition.

Two source qualifications are recorded in the formal statements. The proofs of Lemma 24 and Theorems 25–27 need $Ef$ proper and lower semicontinuous in the strong product topology, as Theorem 18 states. In the forward direction of Theorem 27's optimality equivalence, $Ef(x,\bar u)>-\infty$ is also required: with value $-\infty$, primal optimality need not give a finite pointwise subgradient. The reverse direction has no such added guard. These repairs and the duplicated “$(SP)$” display are documented in the mission notes.

Selected references

• Teemu Pennanen and Ari-Pekka Perkkiö, Dual solutions in convex stochastic optimization, arXiv:2205.15825v1, 2022; later published in Mathematics of Operations Research, 2025. Pinned preprint.

Motivation

Retirement timing is an optimal stopping decision: continuing work earns income but incurs labor cost, while stopping removes both. In the investment model of Jang, Xu and Zheng, the decision also interacts with asset returns and with consumption of basic and luxury goods. The paper separates the retirement decision from the individual's utility specification by moving to a dual state. The resulting free boundary says which dual states favor immediate retirement. A rigorous account of that boundary is useful whenever one wants to compare retirement timing across income, labor-cost or market scenarios without solving a new utility-specific stopping problem.

This mission concerns the near-terminal shape of the boundary in the arXiv:2008.00392v2 version. The paper states that the boundary increases as mandatory retirement approaches and converges to the contemporaneous ratio of labor cost to income. Its printed argument shifts time in a differential operator that the model permits to vary with time. The target below includes the additional condition that makes that shift valid. The original time-dependent claim is therefore not represented as an unconditional theorem.

Setting

There are $n\ge1$ risky assets and two horizons: the mandatory retirement age $T>0$ and a later consumption horizon $\bar T>T$. The deterministic coefficients on $[0,\bar T]$ are the interest rate $r(t)$, discount rate $\rho(t)$, income $I(t)$, labor cost $L(t)$, excess-return vector $\mu(t)$ and volatility matrix $\sigma(t)$. The market price of risk $\vartheta(t)$ solves $\sigma(t)\vartheta(t)=\mu(t)$. The scalar coefficients and each component of $\mu$ are positive, continuous and bounded; $\sigma$ is continuous and uniformly elliptic in the sense that $\sigma(t)\sigma(t)^\top$ is bounded above and below by positive multiples of the identity. These are the standing model assumptions on p. 7, supplemented by the relation defining $\vartheta$ on p. 12 of the source.

For a dual state $y>0$ at time $t$, let $Y^{t,y}$ solve the dual state equation

$$dY(u)=Y(u)\bigl((\rho(u)-r(u))\,du-\vartheta(u)^\top dB(u)\bigr),\qquad Y(t)=y.$$

The noise term is represented by the scalar process $Z(u)=\int_0^u\vartheta(v)^\top dB(v)$. Its increments are independent of the past and Gaussian with variance $\int_s^u\|\vartheta(v)\|^2\,dv$. These properties determine the stopping model used here.

The dual stopping value $\mathbb W(t,y)$ is the largest expected discounted net gain from continuing until a stopping time $\tau\in[t,T]$:

$$\mathbb W(t,y)=\sup_{\tau\in[t,T]}\mathbb E\left[ \int_t^\tau e^{-\int_0^u\rho(v)\,dv} \bigl(Y^{t,y}(u)I(u)-L(u)\bigr)\,du\right].$$

This is equation (26), started at $(t,y)$, with the absolute-time discount in equation (25). On $\mathcal S=[0,T)\times(0,\infty)$, the retirement region is $\mathcal R=\{(t,y):\mathbb W(t,y)=0\}$ and the working region is $\mathcal C=\{(t,y):\mathbb W(t,y)>0\}$. The free boundary is $b(t)=\inf\{y>0:\mathbb W(t,y)>0\}$, with $\inf\varnothing=+\infty$.

Formalization targets

Threshold and comparison statements

Proposition 16 describes the two regions by $y\le b(t)$ and $y>b(t)$, and says that higher income or lower labor cost lowers the boundary. Proposition 17 gives the preterminal bound

$$b(t)\le \frac{L(t)}{I(t)}\qquad (0\le t<T).$$

The proof-level milestones state that $\mathbb W(t,y)$ is nondecreasing in $y$ and, under the aged-window conditions below, nonincreasing in $t$. These statements follow the labels and proof passages in the source, pp. 17 and 39–40.

Goal: near-terminal boundary

Assumption 18 fixes an aged interval $[T-\ell,T]$, where $0<\ell\le T$, and asks

$$\frac{I'(t)}{I(t)}\le\rho(t)\le\frac{L'(t)}{L(t)}.$$

The corrected goal also asks that $\rho(t)-r(t)$ and $\|\vartheta(t)\|^2$ be constant on that interval. It then states that $b$ is nondecreasing there and

$$\lim_{t\uparrow T}b(t)=\frac{L(T)}{I(T)}.$$

The left limit is essential: $b(T)=+\infty$ under the paper's empty-set convention, even though the limit from earlier times is finite.

Significance

The boundary turns a stopping-time optimization into a time-and-state decision rule. The upper bound and the terminal ratio supply observable scales for that rule. The comparative-statics statement identifies the direction of change when income rises or labor cost falls while the investment environment stays fixed. Near $T$, the goal says that the threshold moves monotonically toward a ratio involving only the two labor coefficients, despite the stochastic dual state. These are the retirement-region claims of Propositions 16–17 and Theorem 19.

The paper presents analytic arguments for these results; this mission asks for machine-checked Lean proofs of the stated stopping-model claims. The current draft contains definitions and open theorem statements, not verified proofs. It also records two corrections explicitly, so that a future proof cannot silently rely on the false terminal endpoint of Proposition 17 or on time invariance absent from the printed Theorem 19.

Difficulty

The boundary is an infimum of a strict-positive-value region rather than an explicit formula. Showing monotonicity of the value alone does not automatically settle the boundary at points where the value is zero, and a limit of the boundaries needs control of behavior close to the terminal time. The time-dependent generator is a separate obstacle: changing the starting time also changes the future drift and volatility schedule, so the printed time-shift comparison is unavailable without a condition that fixes the generator on the aged interval. Stopping-time suprema add measurability, integrability and finite-value obligations before any order comparison is meaningful.

Formalization scope

Time and the dual state are real-valued. The market has finitely many assets, $n>0$; the retirement horizon $T$ is strictly before the coefficient horizon $\bar T$. Income and labor cost are positive, so $L/I$ is defined throughout the relevant interval. The deterministic $n$-dimensional Wiener integral is encoded by a continuous adapted scalar process with independent Gaussian increments of variance $\int_s^u\|\vartheta(v)\|^2dv$. This retains the law and filtration properties the stopping value uses.

The value $\mathbb W$ is the stopping representation of (25)–(26), not the Sobolev/PDE definition (24). The two differ only through the paper's identification of those formulations. Appendix F's discount from $t$ instead of zero is a positive rescaling and leaves the zero regions and boundary unchanged. Each stopping payoff is required to be integrable within the value's defining set; for the paper's bounded coefficients and lognormal state this is expected for every admissible stopping time. The supremum is taken over actual admissible stopping times and is nonempty because immediate stopping gives zero. Its upper bound is finite under the same model. The formal proof must establish these facts rather than exploit a default value of a real supremum.

The boundary takes values in the extended reals so an empty working set gives $+\infty$. The additional constancy of $\rho-r$ and $\|\vartheta\|^2$ on $[T-\ell,T]$ appears only in the corrected Theorem 19 and its time-comparison milestone. Assumption 18 uses derivatives within that closed interval, including one-sided endpoint derivatives. The paper's utility and wealth-control layer, the verification theorems, and the variational-inequality comparison theorem are outside this stopping-model mission. Reusable contributions include the Gaussian-increment model, integrability and boundedness results for the stopping value, and general facts about thresholds formed from positive-value regions. The claim cannot be discharged by assigning a convenient boundary or by restricting to a constant stopping time: $b$ is computed from the full stopping-time supremum.

Selected references

• H. J. Jang, Z. Q. Xu and H. Zheng, Optimal Investment, Heterogeneous Consumption, and Best Time for Retirement, Operations Research, 2024; source used here: arXiv:2008.00392v2, 2022. arXiv

Motivation

Large language models answer reasoning questions better when they are allowed to write out a chain of thought (CoT) before the final answer, but every generated token costs time and money. A large body of recent work therefore asks models to "think less": prompts such as "be concise" or "use at most 10 words", and training methods that shorten the reasoning trace. These methods trade accuracy for length, and the natural question is how good such a trade can possibly be.

Lee, Che and Peng (2025) study this question empirically on MATH-500, GSM8K and MMLU-Pro Math with 31 prompts and several frontier models. Their key observation is that, question by question, correctness is almost a threshold function of the response length: a model solves a question if and only if its chain of thought is at least as long as a question-specific token complexity. Under this hypothesis they derive the best possible accuracy–length tradeoff over all prompts, and show that existing prompting strategies are far from it (Table 4 of the paper). This mission formalizes that derivation: Theorem 1 of the paper and the steps of its proof in Appendix D.

Setting

Fix one language model and a dataset of $n \ge 1$ questions $i = 1, \dots, n$. A prompt $P$ determines, for each question $i$, a chain of thought of token length $t_i(P) \in \mathbb N$ and a correctness indicator $a_i(P) \in \{0, 1\}$. The accuracy and the average token length of a prompt are

$$\mathrm{Acc}(P) = \frac1n \sum_{i=1}^n a_i(P), \qquad \bar t(P) = \frac1n \sum_{i=1}^n t_i(P).$$

The two optimal tradeoff curves are the optimal accuracy at average budget $T$ and the minimal average length for accuracy $\alpha$:

$$\alpha^*(T) = \max_P \{\mathrm{Acc}(P) : \bar t(P) \le T\}, \qquad T^*(\alpha) = \min_P \{\bar t(P) : \mathrm{Acc}(P) \ge \alpha\}.$$

Assumption 1 (token complexity hypothesis). There are numbers $\tau_i \in \mathbb N \cup \{\infty\}$, the token complexities, such that for every prompt $P$ and question $i$,

$$a_i(P) = \mathbf 1\{t_i(P) \ge \tau_i\}.$$

The value $\tau_i = \infty$ marks a question the model never solves. The paper also assumes the prompts are rich: every vector of token counts $(t_i) \in \mathbb N^n$ is produced by some prompt. The answer is expressed through the empirical quantities

$$F_n(t) = \frac1n \sum_{i} \mathbf 1\{\tau_i \le t\}, \qquad E_n(t) = \frac1n \sum_{i} \tau_i \mathbf 1\{\tau_i \le t\}, \qquad A^* = \frac1n \sum_i \mathbf 1\{\tau_i < \infty\},$$

where $A^*$ is the largest accuracy any prompt can reach.

Formalization targets

Goal: Theorem 1 (corrected), p. 7

Assume Assumption 1, rich prompts, and pairwise distinct finite token complexities. Let $t_T$ be the largest finite $\tau_j$ with $E_n(\tau_j) \le T$ and $q_\alpha$ the smallest finite $\tau_j$ with $F_n(\tau_j) \ge \alpha$. Then for every $T \ge 0$ and every $0 < \alpha \le A^*$,

$$\alpha^*(T) = \frac1n \sum_{i=1}^n \mathbf 1\{\tau_i \le t_T\}, \qquad T^*(\alpha) = \frac1n \sum_{i=1}^n \tau_i\, \mathbf 1\{\tau_i \le q_\alpha\},$$

with both optima attained. As printed, the theorem defines $t_T \equiv \inf\{t \in \mathbb R : E_n(t) = t\}$, which does not depend on $T$, and $q_\alpha = \sup\{t : F_n(t) \le \alpha\}$, which overshoots the quantile; both readings give wrong values on one- and two-question examples. The goal uses the thresholds that the proof and the text describe ("the highest value of τ that the LLM puts into the knapsack", "the α-quantile of the empirical distribution").

Milestones (Appendix D, p. 14)

1. Eq. (8): under Assumption 1, $\mathrm{Acc}(P) = \frac1n\sum_i \mathbf 1\{\tau_i \le t_i(P)\}$ (the page prints the inequality reversed).
2. Eqs. (9)–(10): with rich prompts, $\alpha^*(T)$ and $T^*(\alpha)$ are the optima of the same problems over token-count vectors $t \in \mathbb N^n$.
3. Eqs. (11)–(12): these equal the optima of a 0-1 knapsack with unit rewards and costs $\tau_i$,

$$\max_{x \in \{0,1\}^n} \frac1n \sum_i x_i \quad \text{s.t.} \quad \frac1n \sum_i \tau_i x_i \le T.$$

4. The greedy claim: for $T \ge 0$ the knapsack optimum is $m/n$, where $m$ is the largest number with $\tau_{(1)} + \dots + \tau_{(m)} \le nT$ for the sorted finite token complexities $\tau_{(1)} \le \tau_{(2)} \le \cdots$.
5. The $T^*$ analogue: for $0 \le \alpha \le A^*$ the minimal cost is $\frac1n(\tau_{(1)} + \dots + \tau_{(\lceil n\alpha\rceil)})$.

Milestones 4 and 5 allow ties among the token complexities; the goal's closed form does not.

Significance

Theorem 1 turns an optimization over all conceivable prompting strategies, an infinite and unstructured set, into a formula in the empirical distribution of $n$ numbers. Its consequence, Corollary 1, is that $T^*(A^*)$, the average token complexity of the solvable questions, is a lower bound on the average length of any lossless compression of the chain of thought; the paper's Table 4 uses it to show that current concise prompts leave a 3–11× reduction unrealized. The same characterization explains why adaptive strategies, which spend more tokens on harder questions, are necessary to approach the frontier.

The result has a pen-and-paper proof of a few lines in Appendix D; the prior-art search found no machine-checked version. Formalizing it adds a correct statement: the printed definitions of $t_T$ and $q_\alpha$ are wrong, eq. (8) has a reversed inequality, and the closed form silently needs distinct token complexities. The mission records the correct versions with the counterexamples to the printed ones, and separates the tie-robust greedy form (milestones 4–5) from the CDF form (the goal).

Difficulty

The individual steps are elementary, but the obvious argument skips three points. First, passing from prompts to token vectors uses richness in both directions: an optimal prompt must be matched by a token vector and conversely, and the optima must be shown attained, not merely bounded. Second, the reduction to $t_i \in \{0, \tau_i\}$ must handle questions with $\tau_i = \infty$, which can never be selected. Third, the greedy claim is a statement about every feasible selection, not only the sorted ones, and translating the greedy count into the threshold forms $\mathbf 1\{\tau_i \le t_T\}$ and $\mathbf 1\{\tau_i \le q_\alpha\}$ is exactly where ties break the formula, so distinctness must be used at that step and nowhere else.

Formalization scope

• Model. One LLM, superscript $\pi$ dropped. Questions are Fin n; prompts are an arbitrary type; a Benchmark gives token lengths len : Prompt → Fin n → ℕ and correctness correct : Prompt → Fin n → Bool. Each (prompt, question) pair yields one deterministic chain of thought.
• Token complexities are ℕ∞-valued; $\tau_i = \infty$ is ⊤. Assumption 1 is correct P i = true ↔ τ i ≤ len P i ("above" read as $\ge$, as the displayed formula on p. 5 shows). Every count or sum over $\tau$ filters on $\tau_i \ne \infty$ before converting to a natural number.
• Averages are real numbers with division by $n$; the goal assumes $n \ge 1$.
• Optima are IsGreatest/IsLeast predicates over the set of values achieved by prompts, never sSup/sInf, so empty or unbounded feasible sets cannot produce a junk value.
• Added hypotheses, all disclosed: $n \ge 1$; $T \ge 0$; $0 < \alpha \le A^*$ for the $T^*$ part ($\alpha \ge 0$ in milestone 5); pairwise distinct finite token complexities in the goal only.
• Trivializing formalizations ruled out. The goal quantifies over prompts and links them to $\tau$ only through Assumption 1 and richness; neither $\alpha^*$ nor $T^*$ is defined as its closed form, and the goal is not stated over token vectors or knapsack variables. Richness is satisfiable: the canonical benchmark with prompts $\mathbb N^n$ satisfies both hypotheses for every $\tau$.
• Not formalized: Corollary 1 (a consequence the proof of Theorem 1 does not use), the threshold-classifier estimators of §3, and the empirical results.

The definitions (benchmark, empirical CDF over an ℕ∞-valued family, sorted prefix sums) are self-contained. A proof of the greedy milestones gives a reusable fact about unit-reward knapsacks. Proofs of any milestone and of the goal are welcome, as is a formalization of Corollary 1 on top of the goal.

Selected references

• A. Lee, E. Che, T. Peng, How Well do LLMs Compress Their Own Chain-of-Thought? A Token Complexity Approach, arXiv preprint, 2025. https://arxiv.org/abs/2503.01141 (version v2 is the one formalized).
• J. Wei et al., Chain-of-Thought Prompting Elicits Reasoning in Large Language Models, NeurIPS, 2022. https://arxiv.org/abs/2201.11903

Motivation

In a linear bandit problem, a learner chooses a vector and observes a noisy scalar response that carries information about an unknown parameter. Regret analyses often need to control the sum of the learner's uncertainty in the directions it chooses. The familiar elliptical potential lemma does this when uncertainty is represented by the inverse of a deterministic, successively updated Gram matrix. Bayesian learning presents a different object: the posterior covariance of the unknown parameter given the observations. It changes with the realized data and can increase on an individual sample path. Hamidi and Bayati's technical note establishes a potential bound for this posterior object under general prior and noise distributions and uses it to analyze linear Thompson sampling.

The deterministic lemma and the posterior result answer related but distinct questions. In the deterministic setting, the update is fixed by the chosen vectors. Here, actions may depend on earlier observations and the next posterior covariance is itself random. The mission concerns the latter claim, including the observation model that gives the covariance its meaning.

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space with an increasing filtration $(\mathcal F_t)_{t\ge1}$. An unknown parameter $\Theta^\star\in\mathbb R^d$ obeys $\|\Theta^\star\|_2\le1$ almost surely. At time $t$, the learner chooses an $\mathcal F_t$-measurable action $A_t\in\mathbb R^d$ with $\|A_t\|_2\le1$ almost surely. An observation $Y_t$, measurable at time $t+1$, has conditional mean $\langle\Theta^\star,A_t\rangle$ and conditional variance at most $\sigma^2$ when both $\mathcal F_t$ and $\Theta^\star$ are known. No Gaussian law or independent noise model is part of these assumptions.

Write $\Gamma_t=\operatorname{Var}(\Theta^\star\mid\mathcal F_t)$ for the posterior covariance matrix. The quantity $A_t^\top\Gamma_t A_t$ is the remaining parameter uncertainty in the chosen direction. The matrix function used to measure accumulated uncertainty is

$$f(\Sigma,x)=\log\det(I+x\Sigma),\qquad \Sigma\succeq0,\quad x>0.$$

The matrix order $B\succeq A$ means that $B-A$ is positive semidefinite. Conditional expectations of matrices are taken entrywise. The filtration can contain information beyond the actions and observations; it need not be generated by them.

Formalization targets

The first target is the source's stochastic variance reduction inequality. For every $t\ge1$, almost surely,

$$\mathbb E[\Gamma_{t+1}\mid\mathcal F_t]\preceq\Gamma_t-\frac{\Gamma_t^\top A_tA_t^\top\Gamma_t}{\sigma^2+A_t^\top\Gamma_t A_t}.$$

The matrix potential targets are the concavity of $f(\cdot,x)$ on the positive semidefinite cone and equation (2.2): if $\Sigma'=\Sigma-\Sigma VV^\top\Sigma/(1+V^\top\Sigma V)$, then

$$\log(1+V^\top\Sigma V)+f(\Sigma',x)\le f(\Sigma,x+V^\top V).$$

Two scalar and covariance bounds from the proof complete the milestone list: $x\le2\log(1+x)$ on $[0,1]$, and $A_t^\top\Gamma_t A_t\le1$ almost surely. The main target, a conditional formulation of Theorem 2.1, is

$$\mathbb E\!\left[\sum_{t=1}^{T}A_t^\top\Gamma_t A_t\,\middle|\,\mathcal F_1\right]\le 2\max(\sigma^2,1)\log\det(I+T\Gamma_1)\quad\text{almost surely}.$$

The source prints an unconditional expectation on the left although $\Gamma_1$ can be random. Conditioning on $\mathcal F_1$ supplies a coherent general statement; it becomes the printed display when the initial information is trivial. The goal retains the explicit factor $2\max(\sigma^2,1)$ and the horizon $T$ inside the log determinant.

Significance

The result controls a cumulative, adaptively selected posterior quadratic form using only the initial posterior covariance, the horizon and the conditional noise bound. It permits a regret analysis of linear Thompson sampling without replacing the prior by a Gaussian model. In the source, this bound feeds the Bayesian regret theorem for that algorithm; that later theorem is outside this mission's scope. Its proof would also require formalizing the sampling policy and its action-selection law.

The formal development fixes a reusable interface for finite-dimensional posterior covariance under a filtration: a parameter, adapted actions, conditional moments of observations, and an entrywise matrix covariance. It also states the matrix potential claims separately from the probability model, so those claims can serve other analyses of covariance updates. The statements compile locally as open Lean theorems; this mission does not claim machine-checked proofs of them. The deterministic elliptical potential statement already available elsewhere uses a Gram-matrix update and does not establish this posterior result.

Difficulty

Posterior covariance is not pathwise decreasing. The paper's Section 2 example has an observation after which $\Gamma_2>\Gamma_1$. A bound that assumes $\Gamma_{t+1}\preceq\Gamma_t$ for every outcome therefore fails at the first stochastic step. The issue matters especially when actions are adapted: later actions can point toward directions whose posterior variance became large after earlier data. Conditional covariance reduction is a matrix inequality, while the target is a scalar sum of quadratic forms; its potential must remain valid across those different objects.

Formalization scope

Lean uses vectors Fin d → ℝ and the Euclidean dot product, so the unit-ball assumptions mean $v^\top v\le1$. The posterior covariance is the conditional expectation of centered coordinate products. The expectation of a covariance matrix is defined entrywise; matrix order is positive semidefiniteness of the difference. The conditioning sigma-algebra for $Y_t$ is $\mathcal F_t\vee\sigma(\Theta^\star)$, not merely $\mathcal F_t$. Every observation is explicitly square-integrable, so Lean's totalized conditional variance cannot silently return zero for a non-square-integrable input. The source's bound on the parameter already supplies its integrability.

Rounds start at $1$; the finite sum uses $1\le t\le T$. At $T=0$ it is empty and both sides of the goal are zero. No positivity assumption on $\sigma$ is imposed, since the statements use $\sigma^2$ and the zero-denominator covariance correction has zero numerator. The log determinant is used on positive semidefinite covariance matrices with nonnegative scalar argument, where its determinant is positive. The paper's square-root factorization of $\Sigma'$ is represented by its equal direct matrix formula. A deterministic Gram matrix in place of $\Gamma_t$, an independent-observation construction in place of the conditional-moment model, or a supremum-norm ball would change the theorem. The separate matrix and probability lemmas, conditional expectation infrastructure, and finite-dimensional matrix order are the principal reusable components.

Selected references

• Nima Hamidi and Mohsen Bayati, The Elliptical Potential Lemma for General Distributions with an Application to Linear Thompson Sampling, technical note, Operations Research, 2023; formalization source: arXiv:2102.07987v3, 2022, §2 and Appendix A.

Motivation

Firms increasingly record what they learn about a customer in one transaction and use it to price the next one. Regulators treat this data tracking as a privacy problem; the consumer-protection question is whether consumers, as a group, lose from it. In a monopoly the answer is typically yes: the seller who learns a consumer's valuation extracts it. Bimpikis, Morgenstern and Saban (Data Tracking under Competition, Operations Research, 2024) show that competition in the market where the data are collected can reverse this. A firm that wants a consumer's data must first win her business, and the competition for that first sale passes the value of the data back to consumers.

The paper builds on the literature on behaviour-based price discrimination (Fudenberg and Villas-Boas, Behavior-based price discrimination and customer recognition, Handbook on Economics and Information Systems, vol. 1, 2006, pp. 377–436) and on the economics of privacy (Acquisti, Taylor and Wagman, The economics of privacy, J. Econ. Literature 54(2), 442–492, 2016). Its distinctive feature is a two-dimensional private type, so that the purchase decision reveals information that matters in a different market.

Setting

A single consumer has a type $\tau=(s,\theta)$ drawn from the uniform distribution $\mu_0$ on $[0,1]^2$. In period 1 two firms sell product 1 on a Hotelling line: firm A at $0$ and firm B at $1$. They set prices $p^A_1\in S_A=[0,1]$ and $p^B_1\in S_B=[-1/2,1]$. The consumer must buy product 1 from exactly one of them, and her utility is $\bar u - s/2-p^A_1$ from A or $\bar u-(1-s)/2-p^B_1$ from B (2.1), with baseline utility $\bar u>0$.

In period 2 firm B alone sells product 2, which the consumer values at $m\theta$; the parameter $m>0$ is the value of consumer data. If she bought product 1 from B, firm B has tracked her: it observes $(s,\theta)$ and can charge a personalized price. Otherwise it knows only the product-1 prices, and it prices product 2 against its belief about the types that bought from A.

The paper compares three settings:

• forward-looking: the consumer chooses her product-1 seller to maximize total utility, anticipating tracking;
• myopic: tracking is the same, but she maximizes product-1 utility only;
• restricted: no tracking, so firm B's period-2 information is the prices alone.

The equilibrium notion is perfect Bayesian equilibrium (Appendix A). It requires sequential rationality of the consumer and of firm B after every pair of product-1 prices, beliefs given by Bayes' rule where it applies, and mutual best responses in product-1 prices. The aggregate consumer surplus $CS^{FL}$, $CS^M$, $CS^R$ is the $\mu_0$-expectation of the consumer's total utility along the equilibrium path.

The forward-looking equilibria correspond to the pure-strategy Nash equilibria of a reduced two-player game $\mathbf G(m)$ (Definition 1, Lemma 2). The interior regime is $m<m_L$, where $m_L$ is the supremum of the $m'$ such that $\mathbf G(\mu)$ has an interior equilibrium for every $\mu\in(0,m']$ (B.32). Numerically $m_L\approx3.98$.

Formalization targets

Goal: Theorem 2

For every $\bar u>0$ and $m\in(0,m_L)$, equilibria exist in all three settings, and every equilibrium triple satisfies

$$CS^R<CS^M\qquad\text{and}\qquad CS^R<CS^{FL}.$$

The goal fixes no numerical value of $m_L$. It asserts only the two comparisons with the restricted benchmark, which is what the theorem claims.

Milestones

The proof runs through the following chain:

• the characterization of the continuation game after product-1 prices (Lemma 1);
• the reduction to $\mathbf G(m)$ (Lemma 2) and the uniqueness of its equilibrium in the interior regime (Lemma 3);
• the equilibria of the restricted and myopic settings (Propositions 1 and 2), and their surplus closed forms (Claim 20, which gives $CS^M>CS^R$);
• firm A's best response $p^A_1=Z(\bar X,m)$ (Claim 12);
• the forward-looking surplus (C.3) (Claim 21);
• the bound $m_L<4$ (Remark 1), the root equation $N(\bar X^*,m)=0$ (C.4) and the bounds $0<\bar X^*<1/2$ (Claim 22);
• the algebraic reduction $\Gamma=J_1/J_2$ and (C.7), the root exclusion for the polynomial system (C.8), and $F(2)>0$;
• $CS^{FL}>CS^M$ (Claim 23).

The strict chain $CS^{FL}>CS^M>CS^R$ is stronger than the goal.

Significance

Theorem 2 is the paper's headline. With competition in the market where data are collected, tracking raises aggregate consumer surplus, and this holds even when consumers ignore the consequences of their purchases. Firm B pays for the data in advance with lower product-1 prices, and firm A must respond. The policy content is that blanket restrictions on tracking can hurt consumers when the data-collecting market is competitive. The paper's Proposition 3 contrasts this with a monopoly in both markets (for $\bar u\ge1/2$). There, tracking lowers consumer surplus for myopic consumers, and also for forward-looking ones when $m\ge4(1-\bar u)$. That contrast is outside this mission.

The paper proves Theorem 2 with pen and paper and a computer-algebra step. The step solving (C.8) uses a Gröbner basis computed in Mathematica, and $F(2)>0$ rests on a numerical evaluation. None of it is machine-checked. A formal proof would certify the following:

1. the equilibrium analysis of a dynamic game with incomplete information, off-path beliefs and a continuum of types;
2. the elimination step;
3. the numerical sign.

The polynomial facts (C.7) and (C.8) are self-contained and can be attacked independently of the game theory.

Difficulty

The obvious argument would compute the forward-looking equilibrium in closed form and compare surpluses. That argument fails, because no closed form exists. Firm B's profit in $\mathbf G(m)$ is not quasiconcave in its own price, so existence and uniqueness of the equilibrium hold only on an interval $(0,m_L)$ whose endpoint is known only numerically. The equilibrium dispersion $\bar X^*(m)$ is defined implicitly as the root of $N(\cdot,m)$, which contains a square root.

Comparing $CS^{FL}$ with $CS^M$ therefore requires showing that a continuous function of $m$, defined through that implicit root, has no zero on $(0,m_L)$. Doing this by hand is not feasible. The paper eliminates variables algebraically and then evaluates the sign at one point.

On the game-theoretic side, the dynamic game has a continuum of information sets. Lemma 1 must pin down beliefs and prices after every off-path price pair. Without that, firm deviations cannot be evaluated, and Lemma 2 fails.

Formalization scope

The formalization commits to the following conventions:

• Types are pairs in $\mathbb R\times\mathbb R$, and $\mu_0$ is the product of Lebesgue measure on $[0,1]$ with itself. Action spaces are $S_A=[0,1]$ and $S_B=[-1/2,1]$ in all three settings (footnote 20). Product 1 is always bought.
• An equilibrium is a relational perfect Bayesian equilibrium: product-1 prices, together with a continuation after every price pair in $S_A\times S_B$. A continuation consists of the following:
  • the consumer's mixed period-1 choice;
  • firm B's tracked prices, untracked price and untracked belief.
• Within a continuation, the conditions are:
  • the consumer is optimal at every type;
  • firm B is optimal at every tracked type and at the untracked information set;
  • with tracking, the belief is the Bayes posterior whenever the untracked event has positive prior mass;
  • in the restricted setting, the belief is $\mu_0$.
• The consumer buys product 2 if and only if its price is at most $m\theta$. This tie-break is forced at tracked nodes and has probability zero elsewhere. Firm B prices product 2 with pure strategies.
• The consumer's choice and the tracked prices are $\mu_0$-a.e. measurable, so every expectation is a genuine integral of a bounded function.
• "$m<m_L$" is the predicate "there is $m'>m$ with an interior equilibrium of $\mathbf G(\mu)$ for all $\mu\in(0,m']$". It is stated without a real supremum, which Lean sets to $0$ on unbounded sets.
• $\psi_x(0,m)=2$ (footnote 34).

Consumer surplus is the integral of realized utility under equilibrium play. It is not defined by the closed forms (C.1) or (C.3), and the goal never substitutes the paper's equilibrium prices; doing either would make the comparison definitional. The goal also asserts existence in each setting, so it cannot hold vacuously.

The development is self-contained apart from the platform's generic pure-Nash predicate CarbonDoubleCount.Planner.IsPureNash. Solvers will need a few pieces of infrastructure:

• computing integrals over the uniform square of piecewise-linear indicator regions;
• an implicit-function argument for continuity of $\bar X^*$;
• a certified root exclusion for (C.8), for example by a resultant or a sum-of-squares certificate.

Proofs of individual milestones are welcome independently. The polynomial items (C.7) and (C.8) and the restricted-setting Proposition 1 are natural first targets.

Selected references

• K. Bimpikis, I. Morgenstern, D. Saban, Data Tracking under Competition, Operations Research, 2024. https://doi.org/10.1287/opre.2023.2489
• D. Fudenberg, J. M. Villas-Boas, Behavior-based price discrimination and customer recognition, in T. Hendershott (ed.), Handbook on Economics and Information Systems, vol. 1, Elsevier, 2006, pp. 377–436 (cited as in the paper's reference list).
• A. Acquisti, C. Taylor, L. Wagman, The economics of privacy, Journal of Economic Literature 54(2), 2016. https://doi.org/10.1257/jel.54.2.442
• D. Cox, J. Little, D. O'Shea, Ideals, Varieties, and Algorithms, 4th ed., Springer, 2015. https://doi.org/10.1007/978-3-319-16721-3

Motivation

Classical utility maximization fixes a utility function at a terminal horizon and optimizes backwards. Forward investment performance processes (FIPPs), introduced by Musiela and Zariphopoulou (2008; 2010), drop the fixed horizon: the investor's preferences are a random field $U_t(x)$ specified today and updated forward in time, in such a way that every past optimal decision remains optimal. Constructing FIPPs in incomplete markets with jumps is the central technical question of this literature.

Power FIPPs, $U_t(x)=e^{D_t}x^p/p$, are the forward analogue of constant relative risk aversion utility. Choulli and Ma (2017, Theory Probab. Appl. 61) characterized them for locally bounded price processes without constraints, using minimal Hellinger martingale densities. Bo, Capponi and Zhou (arXiv:1811.11899, Mathematics of Operations Research, 2023) remove local boundedness and add convex compact portfolio constraints. They characterize exactly which scalar semimartingales $D$ make $e^{D}x^p/p$ a FIPP, through an equation (3.7) between the characteristics of $D$ and an optimization problem over the constraint set. This mission formalizes that characterization, Theorem 3.3 of the paper.

Setting

Fix a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ with the usual conditions and $\mathcal F_0$ trivial. Time is $t\in[0,\infty)$.

• Returns. $R$ starts at zero and is an $\mathbb R^n$-valued càdlàg semimartingale. Relative to the truncation $h(u)=u\mathbf 1_{\{|u|\le1\}}$ it has differential characteristics $(b,c,F)$: drift rate $b_t$, diffusion matrix $c_t$, and jump kernel $F_t(du)$, so that its jump measure $\mu$ has compensator $\nu(dt,du)=F_t(du)\,dt$.
• Strategies and wealth. A predictable $\pi_t\in\mathbb R^n$ gives the fractions of wealth held in the assets. Wealth is $X^{\pi,x}=x\,\mathcal E(\pi\cdot R)$, where $\mathcal E$ is the Doléans-Dade exponential. Portfolios are constrained to a predictable set $\mathcal C_t(\omega)$. Under (A_C) each $\mathcal C_t(\omega)$ is compact, convex and contains $0$.
• Factor. $D$ is a scalar semimartingale with characteristics $(b^D,c^D,F^D)$ relative to $h^D(v)=v\mathbf 1_{\{|v|\le1\}}$. (A_D) requires $(e^v-1-h^D(v))*\nu^D$, or $e^v\mathbf 1_{\{v>1\}}*\nu^D$, to have finite variation.
• Admissibility (Definition 2.1). For a measure $Q\sim P$ and a random field $U^Q$, the class $\Gamma^Q_{\mathcal C}$ consists of the predictable, $\mathcal C$-constrained, $R$-integrable $\pi$ such that $\pi^\top\Delta R\ge-1$, and such that $U^Q_t(x\mathcal E_t(\pi\cdot R))^-$ is of class (DL) under $Q$ for every $x>0$.
• FIPP (Definition 2.2). $U^Q$ is a $Q$-FIPP with optimal $\pi^*\in\Gamma^Q_{\mathcal C}$ if three properties hold: $x\mapsto U^Q_t(x)$ is concave and increasing; $U^Q(X^{\pi,x})$ is a $Q$-supermartingale for every admissible $\pi$; and $U^Q(X^{\pi^*,x})$ is a $Q$-martingale.
• Change of measure. By Lemma 3.1, $e^D=e^{D_0}\mathcal E(M)\mathcal E(V)$, with $M=D^c+(e^v-1)*(\mu^D-\nu^D)$ a local martingale and $V=\int_0^\cdot(b^D+c^D/2+\int(e^v-1-h^D)dF^D)\,ds$. The measure $Q^M$ is given by $dQ^M/dP|_{\mathcal F_t}=\mathcal E_t(M)$. Under $Q^M$, $R$ has characteristics $(b^M,c,F^M)$ and continuous martingale part $R^{M,c}$.
• The objective. For $\pi$ in $\mathcal C_0=\{\pi:F(\{u:\pi^\top u+1<0\})=0\}$,

$$\Phi^M_p(\pi)=\pi^\top b^M+\frac{p-1}{2}\pi^\top c\pi+\int\Big\{p^{-1}(1+\pi^\top u)^p-p^{-1}-\pi^\top h(u)\Big\}F^M(du).$$

Formalization targets

Goal: Theorem 3.3

Let $p\in(-\infty,0)\cup(0,1)$, assume (A_C), (A_D) and $Q^M\in\mathcal Q_M$, and let $\pi^*\in\Gamma^P_{\mathcal C}$. Then $U_t(x)=e^{D_t}x^p/p$ is a $P$-FIPP with optimal strategy $\pi^*$ if and only if the following three conditions hold:

1. $\mathcal E\big(p\pi^*\cdot R^{M,c}+\overline W^M(u)*(\mu-\nu^M)\big)\mathcal E(M)$ is a $P$-martingale, where $\overline W^M_t(u)=\{1+(\pi^*_t)^\top u\}^p-1$;
2. $\Phi^M_p(\pi^*)=\sup_{\pi\in\mathcal C\cap\mathcal C_0}\Phi^M_p(\pi)$, $P\otimes dt$-a.s.;
3. $P\otimes dt$-a.s.,

$$\sup_{\pi\in\mathcal C\cap\mathcal C_0}\Phi^M_p(\pi)+p^{-1}\Big\{b^D+\frac{c^D}{2}+(e^v-1-h^D(v))*F^D\Big\}=0.$$

Milestones

• Lemma 3.1 (p. 8): the multiplicative decomposition $e^D=e^{D_0}\mathcal E(M)\mathcal E(V)$.
• Lemma A.1 (p. 27): an $\varepsilon$–$\delta$ characterization of class (DL).
• Lemma 3.2 (i)–(ii) (p. 9): $\Gamma^P_{\mathcal C}=\Gamma^{Q^M}_{\mathcal C}$, and $U$ is a $P$-FIPP iff $U^V=U_0\mathcal E(V)$ is a $Q^M$-FIPP.
• Lemma 3.4 (p. 10): the FIPP property forces the integrability needed for (3.10), and it forces (3.7).

Significance

The result reduces a question about a family of supermartingales indexed by all admissible strategies to a pointwise condition. Equation (3.7) links the drift, diffusion and jump rates of $D$ to the value of a concave maximization over the constraint set, and the maximizer is the optimal strategy. The paper uses this to build power FIPPs in factor models, by an integral representation (Theorem 4.5), and through a forward HJB equation (Theorem 5.2). Its examples cover Lévy markets with constraints, where the optimal strategy is constant.

None of this is formalized anywhere. Mathlib has martingales, stopping times, the predictable $\sigma$-algebra and localizing sequences, but it has no predictable characteristics, compensated jump integrals, continuous martingale parts, Doléans-Dade exponential or class (DL). The mission's first two definitions build a relational version of that layer. Each object in it is pinned down by a characterization theorem from Jacod and Shiryaev. The layer can be reused by any formalization of jump-semimartingale finance or of limit theorems for semimartingales.

Difficulty

The obvious route is a verification argument for each strategy: write $U^V(X^{\pi,x})$ as a stochastic exponential (3.10) and read off its drift $dV/dt+p\Phi^M_p(\pi)$. This route breaks in three places.

1. Necessity needs integrability first. In the "only if" direction, writing (3.10) requires $p\pi\in L^2_{loc}(R^{M,c})$ and $W^\pi\in G_{loc}(\mu)$. These are not given; they must be derived from the FIPP property itself (Lemma 3.4).
2. The supremum is over all of $\mathcal C\cap\mathcal C_0$. Passing from "drift $\le0$ for every admissible $\pi$" to the pointwise supremum in (3.7) needs near-maximizing predictable selections of $\mathcal C\cap\mathcal C_0$ that are themselves admissible. For $p<0$ that includes the class (DL) clause.
3. Supermartingales from drift signs. In the "if" direction, a negative drift gives only a local supermartingale. For $p\in(0,1)$, positivity upgrades it to a supermartingale. For $p<0$ the upgrade goes through class (D), which is why Definition 2.1 carries the class (DL) clause.

Without local boundedness, $\Phi^M_p$ can take the value $+\infty$ (for $p>0$) or $-\infty$ (for $p<0$), and first-order conditions are unavailable.

Formalization scope

Time is ℝ≥0, and processes are ℝ≥0 → Ω → (Fin n → ℝ). Local martingales are the published EthierKurtz.IsSourceLocalMartingale.

• Calculus layer. It is relational:
  • characteristics are the martingale-problem characterization of Jacod–Shiryaev II.2.21;
  • $X^c$ and $W*(\mu-\nu)$ are pinned down by I.4.18–I.4.19;
  • $\beta\cdot X^c$ is pinned down by its brackets;
  • $\mathcal E$ is the explicit formula I.4.64;
  • class (DL) is the classical uniform-integrability form.
• Standing conditions are explicit hypotheses: $R_0=0$, right-continuity and completeness of the filtration, and $\mathcal F_0$ trivial.
• Disclosed choices:
  • $R$-integrability is the class of integrands whose four canonical-decomposition integrals exist separately (a subclass containing every bounded predictable strategy), computed under $P$;
  • $(b^M,F^M)$ and $R^{M,c}$ are hypotheses: the characteristics and continuous part of $R$ under $Q^M$, rather than the Girsanov formulas (2.7)–(2.8);
  • at zero wealth the fields take their limit values, $0$ for $p>0$ and $-\infty$ for $p<0$;
  • $\Phi^M_p$ is extended-real-valued;
  • $\pi^*$ is fixed on both sides of the equivalence;
  • Lemma A.1 adds progressive measurability.
• Ruled out: trivializing formalizations. Neither the FIPP, nor the admissible class, nor the wealth is defined through (3.10) or conditions (i)–(iii), and no calculus object is a free parameter without its characterization. A sorry-free sanity file shows that every hypothesis of the goal holds for a degenerate market.

Welcome contributions:

• proofs of the milestones, Lemma A.1 first, since it needs only Mathlib;
• general lemmas for the calculus layer: uniqueness of the relational objects, Yor's formula, Girsanov for characteristics;
• the paper's display (3.10).

Selected references

• L. Bo, A. Capponi, C. Zhou, Power forward performance in semimartingale markets with stochastic integrated factors, Mathematics of Operations Research, 2023; arXiv:1811.11899v4 (the version formalized). https://arxiv.org/abs/1811.11899
• M. Musiela, T. Zariphopoulou, Optimal asset allocation under forward exponential criteria, Markov Processes and Related Topics: A Festschrift for T. G. Kurtz, IMS Collections 4, 2008, 285–300. http://dx.doi.org/10.1214/074921708000000435
• M. Musiela, T. Zariphopoulou, Portfolio choice under space-time monotone performance criteria, SIAM J. Financial Math., 2010.
• T. Choulli, J. Ma, Explicit description of HARA forward utilities and their optimal portfolios, Theory Probab. Appl. 61, 2017, 57–93.
• J. Jacod, A. N. Shiryaev, Limit Theorems for Stochastic Processes, Springer, 1987.
• M. Nutz, Power utility maximization in constrained exponential Lévy models, Mathematical Finance 22, 2012, 690–709.