Binary entropy

def binary_entropy (x : ℝ) [0 ≤ x ≤ 1] := 
- x log₂ x - (1-x) log₂(1-x)