differentiableAt_qaryEntropy — Mathlib

English

For hp0: p ≠ 0 and hp1: p ≠ 1, qaryEntropy q is differentiable at p.

Русский

Пусть p ≠ 0 и p ≠ 1. Тогда qaryEntropy q дифференцируема в точке p.

LaTeX

$$$ p \neq 0 \land p \neq 1 \Rightarrow \mathrm{DifferentiableAt}(qaryEntropy q) p $$$

Lean4

@[fun_prop]
theorem differentiableAt_qaryEntropy (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) : DifferentiableAt ℝ (qaryEntropy q) p := by
  unfold qaryEntropy; fun_prop (disch := assumption)

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