hasDerivAt_qaryEntropy — Mathlib

English

The derivative of qaryEntropy q with respect to p is log(q − 1) + log(1 − p) − log p.

Русский

Производная по p от qaryEntropy q равна log(q − 1) + log(1 − p) − log p.

LaTeX

$$$ \frac{d}{dp} qaryEntropy q(p) = \log (q - 1) + \log (1 - p) - \log p $$$

Lean4

theorem hasDerivAt_qaryEntropy (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) :
    HasDerivAt (qaryEntropy q) (log (q - 1) + log (1 - p) - log p) p :=
  deriv_qaryEntropy hp₀ hp₁ ▸ (differentiableAt_qaryEntropy hp₀ hp₁).hasDerivAt

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