Zulip Chat Archive

Stream: new members

Topic: deriv2


view this post on Zulip 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

view this post on Zulip Lucas Viana Reis (Dec 07 2020 at 23:51):

Maybe I should ask in #maths ?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Lucas Viana Reis (Dec 08 2020 at 00:53):

Ok, thanks! I will try

view this post on Zulip Yury G. Kudryashov (Dec 08 2020 at 04:44):

I can add iterated derivatives of log to #5116.

view this post on Zulip Yury G. Kudryashov (Dec 08 2020 at 04:45):

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

view this post on Zulip Yury G. Kudryashov (Dec 08 2020 at 04:46):

BTW, deriv log x = 1 / x everywhere

view this post on Zulip Yury G. Kudryashov (Dec 08 2020 at 04:47):

This is a part of #5116

view this post on Zulip 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