## Stream: maths

### Topic: deriv

#### Patrick Massot (Jul 10 2020 at 12:38):

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 (Jul 10 2020 at 14:39):

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

#### Patrick Massot (Jul 10 2020 at 14:46):

What? I want to invoke definitions only.

#### Patrick Massot (Jul 10 2020 at 14:47):

Did I mess up my statement?

#### Gabriel Ebner (Jul 10 2020 at 14:52):

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

#### Patrick Massot (Jul 10 2020 at 14:57):

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

#### Patrick Massot (Jul 10 2020 at 16:05):

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

Last updated: May 10 2021 at 07:15 UTC