Logarithmic exponential derivative chain

Abstract

The logarithm of one minus a negative exponential is smooth on the positive half-line and has a strictly positive third derivative.

Theorem 1.1 (Three derivatives on the positive half-line).

$$\mathrm{ContDiffOn}\left(\mathrm{Real}\left(\right),3,f,\mathrm{Ioi}\left(0\right)\right)\wedge (\forall x:\mathrm{Real}\left(\right),0<x⟹(\mathrm{deriv}\left(f,x\right)=\frac{1}{(\exp \left(x\right)-1)}\wedge \mathrm{iteratedDeriv}\left(2,f,x\right)=-\frac{\exp \left(x\right)}{(\exp \left(x\right)-1{)}^2}\wedge \mathrm{iteratedDeriv}\left(3,f,x\right)=\frac{\exp \left(x\right)(\exp \left(x\right)+1)}{(\exp \left(x\right)-1{)}^3}\wedge 0<\mathrm{iteratedDeriv}\left(3,f,x\right)))$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Interpolation/LogOneSubExpDerivatives.log_one_sub_exp_derivatives (✓ std3). ∎

Source. Repository-derived.

Commentary.

Here f(t) is log(1-exp(-t)). For t greater than zero the logarithm’s argument is positive. Differentiation on this open set gives the three displayed rational expressions. The numerator and denominator in the third expression are strictly positive. Smoothness is asserted on the positive half-line.

References

• Truth anchor: D5/S3/Analytic/Interpolation/LogOneSubExpDerivatives.log_one_sub_exp_derivatives