Dyadic Cost Support Lines

Abstract

Affine supporting inequalities for the classical dyadic cost on the five-outcome real simplex.

Definition 1.1 (Dyadic residual).

$$\forall I:Type,[\mathrm{Fintype}\left(I\right)],\forall p:I\to \mathbb{R},\forall d:\mathbb{N},R\left(p,d\right)=2^d-\sum _{i\in I}\lfloor 2^{d}p\left(i\right)\rfloor$$

Formalization. D5/S3/Arith/FibonacciAtomic/DyadicSupportLines.residual (✓ std3).

Citation. Jeremie Lumbroso (2013). Optimal Discrete Uniform Generation from Coin Flips, and Applications. URL: https://arxiv.org/abs/1304.1916v1.

Commentary.

R(p,d) counts unassigned dyadic cylinders algebraically. The floor is the integer floor. For a nonnegative real probability vector with m coordinates summing to one, R(p,d) is an integer between zero and m-1. Zero coordinates and terminating dyadic expansions are included.

Definition 1.2 (Classical dyadic tail cost).

$$\forall I:Type,[\mathrm{Fintype}\left(I\right)],\forall p:I\to \mathbb{R},L\left(p\right)=\sum _{d\in \mathbb{N}}\frac{R\left(p,d\right)}{2^d}$$

Formalization. D5/S3/Arith/FibonacciAtomic/DyadicSupportLines.cost (✓ std3).

Citation. Jeremie Lumbroso (2013). Optimal Discrete Uniform Generation from Coin Flips, and Applications. URL: https://arxiv.org/abs/1304.1916v1.

Commentary.

L(p) is the real infinite sum of these normalized residuals. The geometric bound (m-1) divided by 2 to the power d gives summability on each finite simplex. The series expression is the classical Knuth-Yao DDG cost recalled by Lumbroso, Section 2.1. The support theorem below concerns this numerical series. Both definitions accept arbitrary finite real vectors. Lean takes an unsummable real tsum to be zero; values outside the probability simplex do not represent sampling costs.

Theorem 1.3 (Five-outcome support lines).

$$\forall p:\mathrm{Fin}\left(5\right)\to \mathbb{R},(((\forall i:\mathrm{Fin}\left(5\right),0\le p\left(i\right))\wedge \sum _{i\in \mathrm{Fin}\left(5\right)}p\left(i\right)=1)\Rightarrow (\mathrm{Summable}\left(d:\mathbb{N}\mapsto \frac{R\left(p,d\right)}{2^d}\right)\wedge \forall t:\mathbb{R},(t=\min \left(p\right)\Rightarrow (0\le t\wedge (t\le \frac{1}{5}\wedge (16t\le L\left(p\right)\wedge 48t-6\le L\left(p\right)))))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/DyadicSupportLines.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every real probability vector on Fin(5), let t be its smallest coordinate. The series is summable, 0 <= t <= 1/5, and both 16t <= L(p) and 48t-6 <= L(p) hold. No rationality or strict positivity hypothesis is imposed. For positive t, in the five consecutive intervals ending at 1/16, 1/8, 5/32, 1/6 and 3/16, finite dyadic bucket budgets give partial-cost bounds 1, 2, 5/2, 11/4 and 3. Above 3/16 the vector q(i)=16p(i)-3 is again a probability vector and L(p)=27/8+L(q)/16. Iterating an error bound of size 4/16^n and taking its zero limit proves the second supporting line, including the uniform law. The two bounds supply necessary inequalities and assert no attainment claim for each prescribed smallest coordinate.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/DyadicSupportLines.cost
• Truth anchor: D5/S3/Arith/FibonacciAtomic/DyadicSupportLines.residual
• Truth anchor: D5/S3/Arith/FibonacciAtomic/DyadicSupportLines.result