hasDerivAt_binEntropy — Mathlib

English

Binary entropy has derivative log(1 − p) − log p.

Русский

Бинарная энтропия имеет производную log(1 − p) − log p.

LaTeX

$$$ \frac{d}{dp} \ binEntropy(p) = \log(1 - p) - \log p $$$

Lean4

/-- Binary entropy has derivative `log (1 - p) - log p`. -/
theorem hasDerivAt_binEntropy (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) : HasDerivAt binEntropy (log (1 - p) - log p) p :=
  deriv_binEntropy _ ▸ (differentiableAt_binEntropy hp₀ hp₁).hasDerivAt

Похожие утверждения