Papers With

← All papers
First page of A weak Hellinger inequality for noisy Boolean channels

A weak Hellinger inequality for noisy Boolean channels

Polona Durcik, Marco Fraccaroli, Joris Roos

cs.IT Sep 22, 2026 · v1 math.CO
formalization verification combinatorics
Read PDF arXiv abstract Code
TL;DR
The three-parameter inequality underlying the weak Hellinger bound is formally verified in Lean 4 using computer-assisted positivity checks.
Abstract
A weak form of the Hellinger conjecture of Anantharam, Bogdanov, Chakrabarti, Jayram, and Nair for the binary symmetric channel is proved: dictator functions maximize Hellinger $Φ$-entropy among all Boolean functions of the input and all one-bit statistics of the output of a noisy channel. The technical heart of the matter is an explicit inequality in three real parameters, which is proved using explicit polynomial approximations and computer-assisted positivity checks. The results are also formally verified in Lean 4.
Problem

The Hellinger conjecture of Anantharam et al. strengthens the Courtade-Kumar conjecture, asserting dictator functions maximize Hellinger information over noisy binary symmetric channels. Beyond high-noise regimes it remains open.

Approach

A weak form of the conjecture is proved: dictator functions maximize Hellinger Φ-entropy among Boolean functions of the input and one-bit statistics of the output. The core reduction leads to an explicit three-parameter inequality F(s,c,d)≥0. This inequality is established via explicit polynomial approximations and computer-assisted positivity checks, and the results are formally verified in Lean 4.

Results

The weak Hellinger inequality is proved, with equality characterized precisely, and the three-point inequality and derived results are formally verified in Lean 4.