affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

tweaks to constants in weightedmean.v #125

Closed hoheinzollern closed 3 months ago

hoheinzollern commented 3 months ago

Improves bound to eps <= 1 / 126