deriv_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 deriv_qaryEntropy (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) : deriv (qaryEntropy q) p = log (q - 1) + log (1 - p) - log p :=
  by
  unfold qaryEntropy
  rw [deriv_fun_add]
  ·
    simp only [Int.cast_sub, Int.cast_natCast, Int.cast_one, differentiableAt_fun_id, deriv_mul_const, deriv_id'',
      one_mul, deriv_binEntropy, add_sub_assoc]
  all_goals fun_prop (disch := assumption)

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