QuantumInfo.ClassicalInfo.ForMathlib.Analysis.SpecialFunctions.Log.NegMulLog

3 declarations

theorem

$-x \log x$ is strictly increasing on $[0, e^{-1}]$

The function $f(x) = -x \log x$ is strictly monotonically increasing on the closed interval $[0, e^{-1}]$ .

theorem

$-x \log x$ is strictly decreasing on $[e^{-1}, \infty)$

The function $f(x) = -x \log x$ (with $f(0)=0$ ) is strictly decreasing on the interval $[e^{-1}, \infty)$ . Here, $\exp(-1)$ denotes the value $e^{-1}$ , and `Set.Ici` denotes the left-closed infinite interval starting from that point.

theorem

$-x \log x \le e^{-1}$ for $x \ge 0$

#negMulLog_le_rexp_neg_one

For any real number $x \ge 0$ , the function $-x \log x$ (denoted as `negMulLog x`) satisfies the inequality $-x \log x \le e^{-1}$ .

QuantumInfo.ClassicalInfo.ForMathlib.Analysis.SpecialFunctions.Log.NegMulLog

−xlog⁡x-x \log x−xlogx is strictly increasing on [0,e−1][0, e^{-1}][0,e−1]

−xlog⁡x-x \log x−xlogx is strictly decreasing on [e−1,∞)[e^{-1}, \infty)[e−1,∞)

−xlog⁡x≤e−1-x \log x \le e^{-1}−xlogx≤e−1 for x≥0x \ge 0x≥0

$-x \log x$ is strictly increasing on $[0, e^{-1}]$

$-x \log x$ is strictly decreasing on $[e^{-1}, \infty)$

$-x \log x \le e^{-1}$ for $x \ge 0$