{"id":"palomar/PALOMAR-2026-10-17-000010","url":"https://github.com/JD-Jones-ASES/renyi-monotonicity/tree/f990878ac03c85b08e80f8b169cbec5941d34e6a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-17-000010-v1.json","repo":"https://github.com/JD-Jones-ASES/renyi-monotonicity","tags":["math.PR","cs.IT","msc:60E15","msc:94A17","msc:60G50","entropy-inequalities","bernoulli-sums","information-theory","lean-formalization"],"score":0,"title":"Rényi and Tsallis entropy monotonicity for Bernoulli sums","trust":"high","domain":"math.PR","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.PR","summary":"Lean formalization of coordinatewise Rényi and Tsallis entropy monotonicity for finite independent Bernoulli sums on the closed half cube, for every real order in [0,2], as stated in Hillion-Johnson Conjecture 4.4. The complete core proves both entropy comparisons and the finite inverse-score association inequality. Concrete coefficient-law and entropy definitions are checked separately. VERIFICATION.md defines exact-source Linux acceptance and distinguishes historical association-only checkpoints.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-17","reactions":{},"formalized":true,"formalizes":[{"title":"A proof of the Shepp-Olkin entropy monotonicity conjecture","identifier":"https://arxiv.org/abs/1810.09791v1","relationship":"formalizes"}]}