deriv

Stream: maths

[Patrick Massot]

I'm trying to understand the calculus library a bit. How are we meant to prove:

import analysis.calculus.local_extr

open_locale topological_space
open set filter asymptotics

example {f : ℝ → ℝ} {a : ℝ} (h : differentiable_at ℝ f a) :
  is_o (λ x, f x - f a - (deriv f a)*(x -a)) (λ x, x - a) (𝓝 a) :=
sorry

[Heather Macbeth]

Do you want to invoke the mean value theorem (docs#exists_deriv_eq_slope) or prove it directly?

[Patrick Massot]

What? I want to invoke definitions only.

[Patrick Massot]

Did I mess up my statement?

[Gabriel Ebner]

I think you're looking for docs#differentiable_at.has_deriv_at

[Patrick Massot]

Thanks, this is clearly one of the pieces I missed.

[Patrick Massot]

Returning to this, I see this was actually the only missing pieces (modulo multiplying things on the right vs on the left)