strictConcave_binEntropy — Mathlib

English

For hp0: p ≠ 0 and hp1: p ≠ 1, HasDerivAt (qaryEntropy q) with derivative log(q − 1) + log(1 − p) − log p at p.

Русский

Пусть p ≠ 0 и p ≠ 1. Тогда имеет место производная: производная qaryEntropy q равна log(q − 1) + log(1 − p) − log p.

LaTeX

$$$ \text{HasDerivAt}(qaryEntropy\ q)(\log (q - 1) + \log (1 - p) - \log p) $.$$

Lean4

theorem strictConcave_binEntropy : StrictConcaveOn ℝ (Icc 0 1) binEntropy :=
  qaryEntropy_two ▸ strictConcaveOn_qaryEntropy

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