differentiableAt_binEntropy — Mathlib

English

binEntropy is differentiable at p if and only if p ≠ 0 and p ≠ 1.

Русский

Функция binEntropy дифференцируема в p тогда и только тогда, когда p ≠ 0 и p ≠ 1.

LaTeX

$$$\text{DifferentiableAt}(\mathbb{R}, \mathbb{R}, \mathrm{binEntropy}, p) \iff p \neq 0 \wedge p \neq 1$$$

Lean4

@[fun_prop]
theorem differentiableAt_binEntropy (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) : DifferentiableAt ℝ binEntropy p :=
  by
  rw [ne_comm, ← sub_ne_zero] at hp₁
  unfold binEntropy
  simp only [log_inv, mul_neg]
  fun_prop (disch := assumption)

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