Appendix C, property 1 — $\mathbb Q^\beta$ and $\mathbb T^\beta$ are nondecreasing in $\beta$

Let $X$ be a nonnegative random variable whose law $P$ is a probability measure on $\mathbb R$ with $P((-\infty, 0)) = 0$. If $0 \le \beta_2 \le \beta_1 \le 1$, where $\beta_1 = 1$ is allowed only when $X$ is bounded above ($P((-\infty, M]) = 1$ for some $M$), then

where $\mathbb Q^\beta$ is the $\beta$-quantile value and $\mathbb T^\beta$ the $\beta$-truncated mean (Definition 3, corrected second branch).

This monotonicity lets the proof of Theorem 5 move between the confidence-shifted levels $\beta \pm \lambda_0 \pm (n - \hat n)/n$.

Formalization Note The paper states the property for $X$ supported on $\mathbb R^+$ and arbitrary $\beta_1 \ge \beta_2$. The levels are restricted to $[0, 1]$, and the top level $\beta_1 = 1$ to variables bounded above. At those excluded levels the paper's values are $+\infty$ ($\mathbb Q^1(X)$ for unbounded $X$; the empty defining set for $\beta > 1$), where the inequality holds trivially in the extended reals. Lean's real $\inf \emptyset = 0$ would falsify it there. No case with finite values is excluded.