Provedrejectionenvelopereview-response

Robust envelope law: over a finite family of rows with coordinatewise maxima u_j, every common rejection envelope K satisfies K ≥ Σ_j u_j, and r* = u/Σu attains it

For all $\htmlData{mx=1}{I, J \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=5}{\pi : \htmlData{mx=0}{I} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{J} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}}$ , $\htmlData{mx=3}{u, r : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{K \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=8}{\forall i, j,\ \htmlData{mx=3}{\htmlData{mx=0}{\pi}(\htmlData{mx=1}{i}, \htmlData{mx=2}{j})} \mathrel{\htmlData{mx=7}{\leq}} \htmlData{mx=6}{\htmlData{mx=4}{u}(\htmlData{mx=5}{j})}}$ , $\htmlData{mx=9}{\forall j,\ \htmlData{mx=8}{\exists i,\ \htmlData{mx=3}{\htmlData{mx=0}{\pi}(\htmlData{mx=1}{i}, \htmlData{mx=2}{j})} \mathrel{\htmlData{mx=7}{=}} \htmlData{mx=6}{\htmlData{mx=4}{u}(\htmlData{mx=5}{j})}}}$ , $\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})}}$ , $\htmlData{mx=3}{\sum_{j} \htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})}} \mathrel{\htmlData{mx=4}{=}} 1$ and $\htmlData{mx=10}{\forall i, j,\ \htmlData{mx=3}{\htmlData{mx=0}{\pi}(\htmlData{mx=1}{i}, \htmlData{mx=2}{j})} \mathrel{\htmlData{mx=9}{\leq}} \htmlData{mx=8}{\htmlData{mx=4}{K} \cdot \htmlData{mx=7}{\htmlData{mx=5}{r}(\htmlData{mx=6}{j})}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{I}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}}$ ), then

\begin{aligned} & \htmlData{mx=4}{\sum_{j} \htmlData{mx=3}{\htmlData{mx=1}{u}(\htmlData{mx=2}{j})}} \mathrel{\htmlData{mx=6}{\leq}} \htmlData{mx=5}{K} \\ & \htmlData{mx=0}{\land} \left(\right. 0 \mathrel{\htmlData{mx=12}{<}} \htmlData{mx=11}{\sum_{j} \htmlData{mx=10}{\htmlData{mx=8}{u}(\htmlData{mx=9}{j})}} \\ & \htmlData{mx=7}{\implies} \htmlData{mx=31}{\forall i, j,\ \htmlData{mx=16}{\htmlData{mx=13}{\pi}(\htmlData{mx=14}{i}, \htmlData{mx=15}{j})} \mathrel{\htmlData{mx=30}{\leq}} \htmlData{mx=29}{\left(\htmlData{mx=20}{\sum_{k} \htmlData{mx=19}{\htmlData{mx=17}{u}(\htmlData{mx=18}{k})}}\right) \cdot \left(\htmlData{mx=28}{\frac{\htmlData{mx=23}{\htmlData{mx=21}{u}(\htmlData{mx=22}{j})}}{\htmlData{mx=27}{\sum_{k} \htmlData{mx=26}{\htmlData{mx=24}{u}(\htmlData{mx=25}{k})}}}}\right)}} \left.\right) \end{aligned}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
x ∈ TVariables: I, J range over Type: the statement must hold for every choice. ((I J : Type))
Fintype: Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application: Fintype applied to I. Lean writes f x; papers write f(x). (Fintype I)
x : TVariables: u, r range over J → ℝ: the statement must hold for every choice. ((u r : J → ℝ))
∀For all: The statement after the comma holds for every i, j. (∀ i j, π i j ≤ u j)
∑Summation: Add up r(j) for every j. (∑ j, r j)
∧And: Both hold: (∑ j, u(j)) ≤ K, and 0 < (∑ j, u(j)) → (∀ i, j, π(i, j) ≤ (∑ k, u(k)) · (u(j)/(…. (∑ j, u j ≤ K ∧ (0 < ∑ j, u j → ∀ i j, π…)
⟹Implies: If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (J → ℝ)
∃There exists: At least one i makes the statement after the comma true. (∃ i, π i j = u j)
<Less than: 0 is strictly smaller than r(j). (0 < r j)
πPi: The ratio of a circle's circumference to its diameter, ≈ 3.14159. (π)
≤At most: π(i, j) is less than or equal to u(j). (π i j ≤ u j)
RReal numbers: The real numbers: every point on the number line. (ℝ)
=Equality: π(i, j) and u(j) are the same. (π i j = u j)
·Multiplication: K times r(j). (K * r j)
a/bDivision: u(j) divided by ∑ k, u(k). In Lean, dividing by 0 gives 0. (u j / ∑ k, u k)

theorem vcl-robust-envelope-law {I J : Type} [Fintype I] [Fintype J] (π : I → J → ℝ) (u r : J → ℝ) (K : ℝ) (hu : ∀ i j, π i j ≤ u j) (hut : ∀ j, ∃ i, π i j = u j) (hr : ∀ j, 0 < r j) (hrs : ∑ j, r j = 1) (hK : ∀ i j, π i j ≤ K * r j) :
    ∑ j, u j ≤ K ∧ (0 < ∑ j, u j → ∀ i j, π i j ≤ (∑ k, u k) * (u j / ∑ k, u k))

The order-∞ counterpart of the variational cost law, supplied by an external reviewer (2026-10-05) after the paper said no closed-form variational law for envelopes was known to the authors. If every row in the family satisfies π_j ≤ K r_j then K ≥ Σ_j u_j (sum the tight coordinates), and the proposal u/Σu achieves envelope Σu for all rows at once. Solves the worst-case envelope problem; the Bayesian objective E[max_j π_j/r_j] is different and remains open.

How it was proved

Proved: 5 October 2026
By: Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 19 lines of Lean

Robust envelope law: over a finite family of rows with coordinatewise maxima u_j, every common rejection envelope K satisfies K ≥ Σ_j u_j, and r* = u/Σu attains it

How it was proved

More proved statements