Central Binomial Tail Bounds (Conjecture 6.3)

This repository contains a formal proof of Conjecture 6.3 from the paper "Central Binomial Tail Bounds" by Matus Telgarsky (2009).

Proven Conjecture

The conjecture provides a refined bound for the tail of the binomial distribution using a Gaussian approximation. Specifically, it states an inequality involving the cumulative distribution function of the standard normal distribution and the tail of the binomial distribution.

Theorem Name in Code: arxiv_id0911_2077_conjecture6_3

Original Paper

• Title: Central Binomial Tail Bounds
• Author: Matus Telgarsky
• arXiv ID: 0911.2077
• Link: https://arxiv.org/abs/0911.2077

Formalization and Proof

This conjecture was automatically proven using the Aleph prover system.

The formal statement corresponds to the one found in DeepMind's formal conjectures repository:

• DeepMind Repository: google-deepmind/formal-conjectures
• File: FormalConjectures/Arxiv/0911.2077/Conjecture6_3.lean