## Stream: new members

### Topic: deriv2

#### Lucas Viana Reis (Dec 07 2020 at 19:50):

Hi. Suppose I want to calculate a 2nd derivative like deriv^[2] log x when x>0, that is, of a function whose first derivative is only partially defined.

I know how to prove that x>0 -> deriv log x = 1/x using deriv_log'. But I can't rw this for calculating the 2nd derivative deriv (deriv \$ λ y, log y) x, since I don't have the "inner" hypothesis y>0. How I should proceed?

#mwe :

import analysis.special_functions.exp_log
noncomputable theory

open real

definition ϕ : ℝ → ℝ := λ x, -x * log x

lemma deriv_log {x : ℝ} (hx : x ≠ 0) : deriv log x = x⁻¹ :=
begin
have p := @deriv_log' id x differentiable_at_id hx,
simp only [one_div, deriv_id', id] at p,
exact p,
end

lemma ϕ' (x : ℝ) (hx : x ≠ 0) : deriv ϕ x = -log x - 1 :=
begin
calc
deriv ϕ x = deriv has_neg.neg x * log x + (-x) * deriv log x : deriv_mul _ _
... = - log x - x * deriv log x : by rw deriv_neg; ring
... = - log x - 1 : by rw [deriv_log hx]; finish,
{ finish },
{ finish }
end

lemma ϕ'' (x : ℝ) (hx : x ≠ 0) : deriv^[2] ϕ x = -1 / x :=
begin
sorry
end


#### Lucas Viana Reis (Dec 07 2020 at 23:51):

Maybe I should ask in #maths ?

#### Kevin Buzzard (Dec 08 2020 at 00:02):

I don't know anything about analysis in Lean, but how is the derivative of log any more or less partially defined than log itself?

#### Reid Barton (Dec 08 2020 at 00:05):

Is the problem that somehow you need to know that the derivative away from zero only depends on the function away from zero?

#### Lucas Viana Reis (Dec 08 2020 at 00:13):

Yes, the second derivative to be precise. The API has theorems that give the formula for the first derivative in points where it is defined; but I want the second derivative, and the way the API is built does not make it clear to me how to use those theorems in succession to calculate higher derivatives, when the first derivative itself is partially defined

#### Reid Barton (Dec 08 2020 at 00:19):

I guess you can use docs#filter.eventually_eq.deriv_eq or one of the preceding functions

#### Kevin Buzzard (Dec 08 2020 at 00:29):

Oh I see. Yes I think Yury explicitly mentioned this as a problem at LFTCM when talking about differentiating tan

#### Lucas Viana Reis (Dec 08 2020 at 00:51):

@Reid Barton should I use deriv_within_congr to prove that if x ≠ 0 → f x = g x then x ≠ 0 → deriv f x = deriv g x ? Or is there an easier way?

#### Reid Barton (Dec 08 2020 at 00:53):

I'm not familiar with this area of the library so I don't know whether there is an easier way, but this should work (using the fact that {x | x ≠ 0} is open, hence a neighborhood of any of its elements)

#### Lucas Viana Reis (Dec 08 2020 at 00:53):

Ok, thanks! I will try

#### Yury G. Kudryashov (Dec 08 2020 at 04:44):

I can add iterated derivatives of log to #5116.

#### Yury G. Kudryashov (Dec 08 2020 at 04:45):

(both as deriv^[n] and docs#iterated_deriv

#### Yury G. Kudryashov (Dec 08 2020 at 04:46):

BTW, deriv log x = 1 / x everywhere

#### Yury G. Kudryashov (Dec 08 2020 at 04:47):

This is a part of #5116

#### Yury G. Kudryashov (Dec 08 2020 at 05:03):

At zero it is equal to 1 / 0 = 0 because log is not differentiable.

Last updated: May 16 2021 at 05:21 UTC