Commit 2024-10-02 14:32 3b0dde03

View on Github →

feat: derivative of absolute value (#17149) Compute the derivative of the absolute value: deriv (|·|) x = SignType.sign x.

Estimated changes

added theorem ContDiff.abs
added theorem ContDiffAt.abs
added theorem ContDiffOn.abs
added theorem ContDiffWithinAt.abs
added theorem Differentiable.abs
added theorem DifferentiableAt.abs
added theorem DifferentiableOn.abs
added theorem HasFDerivAt.abs
added theorem HasFDerivAt.abs_of_neg
added theorem HasFDerivAt.abs_of_pos
added theorem HasFDerivWithinAt.abs
added theorem HasStrictFDerivAt.abs
added theorem contDiffAt_abs
added theorem contDiffOn_abs
added theorem contDiffWithinAt_abs
added theorem deriv_abs
added theorem deriv_abs_neg
added theorem deriv_abs_pos
added theorem deriv_abs_zero
added theorem differentiableAt_abs
added theorem differentiableOn_abs
added theorem hasDerivAt_abs
added theorem hasDerivAt_abs_neg
added theorem hasDerivAt_abs_pos
added theorem hasDerivWithinAt_abs
added theorem hasStrictDerivAt_abs