Real.negMulLog_eq_neg
theorem Real.negMulLog_eq_neg : Real.negMulLog = fun x => -(x * x.log)
The theorem `Real.negMulLog_eq_neg` states that the function `Real.negMulLog`, which maps a real number x to the negative of the product of x and the logarithm of x, is equivalent to an anonymous function that performs the same operation, i.e., maps x to the negative of the product of x and the logarithm of x. This is a crucial identity that ensures the consistent definition and behavior of the `Real.negMulLog` function.
More concisely: The theorem `Real.negMulLog_eq_anonymous` asserts that `Real.negMulLog x = -(x * log x)` for all real numbers `x`.
|
Real.deriv_mul_log
theorem Real.deriv_mul_log : ∀ {x : ℝ}, x ≠ 0 → deriv (fun x => x * x.log) x = x.log + 1
The theorem, `Real.deriv_mul_log`, states that for all real numbers `x`, given that `x` is not equal to zero, the derivative of the function `x * log(x)` at point `x` is equal to `log(x) + 1`. In essence, it's showing a formula for the derivative of the function which multiplies a real number `x` by its logarithm, under the condition that `x` is nonzero.
More concisely: For any nonzero real number `x`, the derivative of the function `x => x * log x` is equal to `log x + 1`.
|