Source-linked AI summary
A weak Hellinger inequality for noisy Boolean channels
Polona Durcik, Marco Fraccaroli, Joris Roos
TL;DR
The Hellinger conjecture concerns whether dictator functions maximize Hellinger information revealed by the full noisy output, and the related Courtade–Kumar conjecture remains open beyond the high-noise regime. This paper proves a weak form using one-bit output statistics and a three-parameter inequality, with the formal verification carried out in Lean 4.
Problem
The Hellinger conjecture asks whether dictator functions maximize Hellinger information revealed by the full noisy output, while the Courtade–Kumar conjecture remains open beyond the high-noise regime.
Source: §1 · p. 1Method
The proof reduces the weak claim to an explicit inequality in three real parameters, using Bernstein polynomial approximations, positivity checks, and Lean 4 formalization.
Source: §1 · p. 2, §1.1 · p. 2Results
The paper proves a weak form of the Hellinger conjecture by replacing conditioning on the full channel output Y with conditioning on an arbitrary one-bit statistic g(Y).
Source: §1 · p. 2Takeaways & Limitations
The authors report a definitive formal verification of the result in Lean 4 alongside traditional mathematical arguments.
Source: §1.1 · p. 2The reduction excludes constant f or g and |ρ| = 1 as trivial cases, and proceeds under the assumption that s, c, and d lie in (0, 1).
Source: §3 · p. 17
Abstract
from arXiv · showhide
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 $\Phi$-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.
1. Introduction
The paper proves a weak form of the Hellinger conjecture by restricting the channel information to an arbitrary one-bit statistic of the noisy output. It reduces the proof to a three-parameter inequality and reports formal verification in Lean 4.
1. Introduction
- Beyond the high-noise regime, the Courtade–Kumar conjecture remains open; prior proofs cover sufficiently small |ρ| and later work extended that range.The conjecture says dictator functions attain equality and can be understood as maximizing mutual information on noisy inputs.Source: §1 · p. 1
- In the low-noise limit, the Hellinger conjecture predicts a sharp inequality at exponent 1 for balanced functions as ρ approaches 1.The passage states this as a prediction of the conjecture.Source: §1 · p. 2
- The weak Hellinger result replaces conditioning on the full noisy output Y with conditioning on an arbitrary one-bit statistic g(Y).The stronger conjecture states that Hellinger information revealed by the full output is maximized by dictator functions; it would imply the Courtade–Kumar conjecture by convexity.Source: §1 · pp. 1–2
- The proof reduces the claim to an explicit inequality in three real parameters, proved using Bernstein polynomial approximations and positivity checks.The reduction follows, and its details are also given in the paper.Source: §1 · p. 2
- The authors describe definitive formal verification of the result in Lean 4, in addition to traditional mathematical arguments.The Lean formalization uses rational numbers for the computations; compiling the theorem takes about 40 GB of RAM and 2.5 hours on one author's machine.Source: §1.1 · p. 2
1.1. Formalization in Lean.
- The main Lean statements are human-written, while their proofs are machine-generated.The formalization was completed using Codex/gpt-6-astra-medium under human supervision.Source: §1.1 · p. 2, Statement on use of AI · p. 2
Statement on use of AI.
- The authors report that OpenAI GPT models contributed substantially to developing the three-point inequality through extended discussions.They state that the Lean formalization was completed using Codex/gpt-6-astra-medium under human supervision.Source: Statement on use of AI · p. 2
2. A three-point inequality √
This section establishes a three-point inequality, develops approximation bounds, and identifies its equality cases. The positivity proof reduces the strict case to monotonicity in transformed variables and polynomial positivity on parameterized regions, certified by Bernstein-basis checks and extended by continuity.
2. A three-point inequality √
- Equality holds only when s∈{0,1}, c+d=1, or s=1/2 and c=d.Source: §2 · p. 3
- The auxiliary function K has an integral representation that establishes its positivity and continuity on (0,1)².Source: §2 · p. 4
- For a,b>0 with a+b<1 and |u|<a, Proposition 2.3 proves that ∂aG(a,b,u)>0.Source: §2 · p. 6
- For a,b>0, a+b<1, and |t|<1, δ²β>k(at,b), yielding the strict inequality in (2.4).Source: §2 · p. 6
2.2. Proof of Φ > 0.
- The proof of Φ>0 uses bounds on L, µ, and θ, including 1/3+ x/3 ≤ L(x) ≤ 7/15 + x/15 + 8/15√(1−x).The supplied bounds also give 1/3+η/3 ≤ µ ≤ 1+η(2+z²)/6 and 2η/3 ≤ θ ≤ 2+y².Source: §2 · p. 6, §2.2 · p. 10
- The proof reduces the remaining cases to Γ− > 0 when w ≤ 0, Γ++ > 0 in region (2.24), and Γ+ > 0 elsewhere for w ≥ 0.A further coordinate change expresses these functions using rational functions and one square root.Source: §2.2 · p. 11, §2.3 · p. 11
2.3. Final reduction.
- The bijective parametrization of (a, b) by (j, k) makes the square roots rational and the functions polynomials in t with coefficients rational in j, k.Clearing positive denominators turns F² − Q into a polynomial without square roots.Source: §2.3 · p. 12
2.4. Polynomial inequalities.
- After clearing positive denominators, positivity reduces to proving Qν > 0 on parameter regions Ων, whose substitutions bijectively cover the required domains U±.The proof uses separate polynomial inequalities for the negative-t case and the two nonnegative-t regions.Source: §2.4 · pp. 12–14
2.5. Positivity of the seven polynomials.
- Table 2 reports coefficient counts and thirteen positive witnesses, but the cited passage does not specify the counts or state what properties the witnesses establish.Source: Table 2 · p. 15
2.6. Positivity of F−, F+, F++.
- Continuity along line segments from each region to its center evaluation shows F−, F+, and F++ remain positive throughout their required regions, including boundaries.The substituted expressions are continuous and nonvanishing along each segment, so the intermediate value theorem transfers the positive center evaluation to every point.Source: §2.6 · pp. 16–17
3. Reduction to the three-point inequality
The section reduces the weak Hellinger inequality to a three-point inequality, following. Data processing removes the fourth parameter, leaving a stronger inequality in three parameters to prove.
3. Reduction to the three-point inequality
- Data processing [13] removes the fourth parameter ρ from the intertwined parameters describing (U, V).The section sets U = g(Y) and V = f(X).Source: §3 · p. 17
- The reverse hypercontractivity parameter sp(U, V) is defined for p ∈ (0, 1), with s†(U, V) = lim p→0+ sp(U, V).The definition concerns bounds on conditional expectations of nonnegative b(V).Source: §3 · p. 17
- The proof targets a stronger inequality, identified as Conjecture 5 in, to establish the weak Hellinger inequality (1.4).The section follows the argument in.Source: §3 · p. 17
- The pair (U, V) is parameterized by s = P(U = 1), c = P(V = 1|U = −1), and d = P(V = −1|U = 1).Source: §3 · p. 17
- The argument excludes constant f or g and |ρ| = 1, then assumes s, c, d lie in (0, 1).Source: §3 · p. 17
- Evaluating the infimum at t = s c̄ + s̄ d gives sD(c̄ | d̄) + s̄D(d | c), yielding (3.1) from (2.1).The section writes s†(U, V) using a formula from.Source: §3 · pp. 17–18