Commit 2024-08-18 01:14 6ad8df9e

View on Github →

feat: Binary entropy (#9734) Define the (Shannon) binary and q-ary entropy functions. The binary entropy function is used in information theory; for example, in Shannon's theorems.

Estimated changes

added theorem inv_div_comm
added theorem Real.binEntropy_nonneg
added theorem Real.binEntropy_one
added theorem Real.binEntropy_pos
added theorem Real.binEntropy_zero
added theorem Real.deriv2_binEntropy
added theorem Real.deriv_binEntropy
added theorem Real.deriv_qaryEntropy
added theorem Real.qaryEntropy_one
added theorem Real.qaryEntropy_pos
added theorem Real.qaryEntropy_two
added theorem Real.qaryEntropy_zero
modified theorem Real.continuous_negMulLog