Probe Threshold Optimization

Abstract

A positive probability vector has a unique threshold, a capped quadratic optimizer, and an exact active-set value.

Theorem 1.1 (The probe threshold is unique and globally optimal).

$$\begin{array}{c}\forall \iota :\mathrm{Type},[\mathrm{Fintype}(\iota )]\\ \forall a:(\iota )\to \mathbb{R},\epsilon :\mathbb{R},\\ ((\forall l,(0<a_l))\wedge (\sum _l{a}_l=1)\wedge (0<\epsilon \wedge \epsilon <1))\Rightarrow \\ (v=(l:\iota \mapsto \sqrt{a_l})),(F(x)=((\sum _l{v}_l\cdot x_l{)}^2-\epsilon \cdot \sum _l{x}_l^2)),\\ \exists c:\mathbb{R},((0<c)\wedge (\sum _l\min (a_l,\frac{v_l}{c})=\epsilon )\wedge (x_{\ast }=(l:\iota \mapsto \min (1,c\cdot v_l)))\wedge (H=\{l\mid 1\le c\cdot v_l\})\wedge \\ (d=\sum _{l\in \iota \setminus H}{a}_l)\wedge (S=\sum _{l\in H}{v}_l)\wedge \\ ((\forall l,(0\le {x_{\ast }}_l\wedge {x_{\ast }}_l\le 1)))\wedge \\ ((\forall x:(\iota )\to \mathbb{R},((\forall l,(0\le x_l\wedge x_l\le 1)))\Rightarrow (F(x)\le F(x_{\ast }))))\wedge \\ (d<\epsilon )\wedge \\ (c=\frac{S}{\epsilon -d})\wedge \\ (F(x_{\ast })=\frac{\epsilon \cdot S^2}{\epsilon -d}-(\epsilon \cdot \mathrm{card}(H))))\wedge (\forall c^{\prime }:\mathbb{R},(0<c^{\prime })\Rightarrow (\sum _l\min (a_l,\frac{v_l}{c^{\prime }})=\epsilon )\Rightarrow (c^{\prime }=c)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/ErrorExponents/ProbeThresholdOptimization.probe_threshold_optimization (✓ std3). ∎

Source. Repository-derived.

Commentary.

The threshold balances the capped square-root weights against epsilon. Strict decrease after the uncapped range makes this balance unique.

Linearizing the squared aggregate separates the box optimization by coordinate. Each coordinate is maximized by its capped linear response.

Splitting the coordinates at the cap gives the threshold identity and the exact objective value in terms of the active mass, active square-root sum, and active count.

References

• Truth anchor: D5/S3/Estimation/ErrorExponents/ProbeThresholdOptimization.probe_threshold_optimization
• Dependency: D5/S3/Analytic/Curvature/CardinalSplineRecurrence