derivative of (f x⁻¹)

Stream: Is there code for X?

[Ryan Lahfa]

Do we have quick/direct proofs of:

import analysis.calculus.deriv

lemma deriv.comp_inv {f : ℝ → ℝ} {x: ℝ}
  (hx: x ≠ 0) (hdf: differentiable_at ℝ f (1 / x)): deriv (λ (y: ℝ), f y⁻¹) x = - (deriv f (1 / x)) / x^2 :=
  begin
    simp [← one_div],
    rw [deriv.comp _ hdf],
    field_simp,
    sorry,
    -- simp [one_div, differentiable_at_inv hx],
  end

I have often difficulties to switch back between inv, has_div.div 1 and their composed forms $f \circ (1/x)$, etc.

[Anatole Dedecker]

import analysis.calculus.deriv

lemma has_deriv_at.comp_inv {f : ℝ → ℝ} {x f' : ℝ} (hx : x ≠ 0) (hff' : has_deriv_at f f' x⁻¹) :
  has_deriv_at (λ y, f (y⁻¹)) (-f' / x^2) x :=
begin
  convert hff'.comp x (has_deriv_at_inv $ hx),
  ring
end

lemma deriv.comp_inv {f : ℝ → ℝ} {x: ℝ}
  (hx: x ≠ 0) (hdf: differentiable_at ℝ f x⁻¹): deriv (λ (y: ℝ), f y⁻¹) x = - (deriv f x⁻¹) / x^2 :=
(hdf.has_deriv_at.comp_inv hx).deriv

[Anatole Dedecker]

In my experience it is often easier to use has_deriv_at and then deduce the deriv versions because you avoid boring rewriting to get syntactic equality

[Ryan Lahfa]

Anatole Dedecker said:

In my experience it is often easier to use has_deriv_at and then deduce the deriv versions because you avoid boring rewriting to get syntactic equality

That's the advice I needed! :)