deriv2

Stream: new members

[Lucas Viana Reis]

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]

Maybe I should ask in #maths ?

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[Lucas Viana Reis]

@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]

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]

Ok, thanks! I will try

[Yury G. Kudryashov]

I can add iterated derivatives of log to #5116.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

BTW, deriv log x = 1 / x everywhere

[Yury G. Kudryashov]

This is a part of #5116

[Yury G. Kudryashov]

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