Lean repository linked
Sharp small-deviation inequalities for sums of independent nonnegative random variables
arXiv:2607.23980 · arXiv
Lean formalisations (1)
pengzhang91/Feige at 19c61d6cb556
Linked by the repository’s formalization.yaml.
Project review: author-verified
Audit: awaiting publication.