strictConcaveOn_qaryEntropy — Mathlib

English

qaryEntropy q is strictly concave on [0,1].

Русский

qaryEntropy q строго вогнута на [0,1].

LaTeX

$$$ \operatorname{StrictConcaveOn}(\mathbb{R}, [0,1], p \mapsto qaryEntropy q(p)) $$$

Lean4

theorem strictConcaveOn_qaryEntropy : StrictConcaveOn ℝ (Icc 0 1) (qaryEntropy q) :=
  by
  apply strictConcaveOn_of_deriv2_neg (convex_Icc 0 1) qaryEntropy_continuous.continuousOn
  intro p hp
  rw [deriv2_qaryEntropy]
  · simp_all only [interior_Icc, mem_Ioo]
    apply div_neg_of_neg_of_pos
    · norm_num [show 0 < log 2 by positivity]
    · simp_all only [mul_pos_iff_of_pos_left, sub_pos]

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