Commit 2020-04-16 11:10 846cbabb
View on Github →feat(analysis/calculus): let simp compute derivatives (#2422) After this PR:
example (x : ℝ) : deriv (λ x, cos (sin x) * exp x) x = (cos(sin(x))-sin(sin(x))*cos(x))*exp(x) :=
by { simp, ring }
Excerpts from the docstrings:
The simplifier is set up to prove automatically that some functions are differentiable, or differentiable at a point (but not differentiable on a set or within a set at a point, as checking automatically that the good domains are mapped one to the other when using composition is not something the simplifier can easily do). This means that one can write
example (x : ℝ) : differentiable ℝ (λ x, sin (exp (3 + x^2)) - 5 * cos x) := by simp.
If there are divisions, one needs to supply to the simplifier proofs that the denominators do not vanish, as in
example (x : ℝ) (h : 1 + sin x ≠ 0) : differentiable_at ℝ (λ x, exp x / (1 + sin x)) x :=
by simp [h]
The simplifier is not set up to compute the Fréchet derivative of maps (as these are in general complicated multidimensional linear maps), but it will compute one-dimensional derivatives.
To make sure that the simplifier can prove automatically that functions are differentiable, we tag many lemmas with the simp attribute, for instance those saying that the sum of differentiable functions is differentiable, as well as their product, their cartesian product, and so on. A notable exception is the chain rule: we do not mark as a simp lemma the fact that, if f and g are differentiable, then their composition also is: simp would always be able to match this lemma, by taking f or g to be the identity. Instead, for every reasonable function (say, exp), we add a lemma that if f is differentiable then so is (λ x, exp (f x)). This means adding some boilerplate lemmas, but these can also be useful in their own right.
Tests for this ability of the simplifier (with more examples) are provided in tests/differentiable.lean.