Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC