Evaluating a derivative

Stream: mathlib4

[Alex Meiburg]

Here's a "simple" kind of derivative problem that I believe is currently more difficult than it should be, with what mathlib provides:

theorem d2 : deriv (deriv (fun (x:ℝ) ↦ Real.arctan (1 + Real.tan (x^2 + x)))) 0 = (1/2) := by
  sorry

Something I genuinely expected simp or norm_num might be able to solve. With only one deriv, it's not too bad, you use rw [deriv_arctan ?_] and then this gives you a meaningful expression that norm_num evaluates down. You get a side goal that the value inside is DifferentiableAt 0, which simp can do.

But when it's a second derivative it's very hacky and gross, because deriv_arctan requires having a proof _at a given x_ that it's differentiable at that point; without already knowing that it's differentiable everywhere, you can't do a good rewrite. This would require a have for the rewrite via funext, and also a have for the fact that it's differentiable everywhere ... if it was.

But the argument also isn't differentiable on all of R, because of the tangent function. So the only solutions (that I see) is something where you rewrite the interior to be if DifferentiableAt then [expression] else 0 and argue about the differentiability of _that_, or you deliberately restrict your range to some neighborhood of zero where everything is good and look at derivatives of that function. But then deriv_arctan doesn't fit in nicely.

[Alex Meiburg]

Is there a good way to handle these problems right now? I feel like there _should_ be some layer of abstraction where I can mostly automatically discharge the differentiability sidegoals and just do it "like AP calc". In principle

[Eric Wieser]

I'd argue the best approach for second derivatives is (or should be) to state the result with docs#HasFTaylorSeriesUpTo instead

[Eric Wieser]

Then you have no differentiability side-conditions

[Alex Meiburg]

Or maybe even AnalyticAt, for those cases where it is?

[Alex Meiburg]

That gives me docs#HasFPowerSeriesAt which I don't know is better or worse

[Patrick Massot]

@Tomas Skrivan is there any news about this kind of question?

[Bjørn Kjos-Hanssen]

Another symptom of iterated deriv is that you can have e.g. deriv (deriv f) x = 2 without f being continuous at x.

[Alex Meiburg]

Really? How?

[Frédéric Dupuis]

$f(x) = x^2$, except at 0 where it's equal to 1. The first derivative just happens to be "correct" because of the junk value.

[Bjørn Kjos-Hanssen]

Time to just make derivative f : ℝ → Option ℝ instead?

[Ruben Van de Velde]

No thanks :)

[Patrick Massot]

What about using docs#iteratedDeriv instead?

[Alex Meiburg]

That just unfolded to the above, deriv (deriv _). Is there a better way to use it?

[Patrick Massot]

Hopefully it has some API.

[Eric Wieser]

I think the answer is the docs#HasFTaylorSeriesUpTo I mention above, or something like it

[Eric Wieser]

In the same way that the way to make differentiability assumptions go away for a single deriv is to use HasDerivAt

[Tomas Skrivan]

Here is my attempt at computing the derivative using simp. Unfortunately I had to assume ∀ x, Real.cos x ≠ 0 which is false. As mentioned, to get it completely automatic we should have theorems either for iteratedDeriv or HasFTaylorSeriesUpTo and make sure that automation can work with these.

code

import Mathlib

open Real

section MissingTheorems

@[fun_prop]
theorem DifferentiableAt.tan (x₀ : ℝ) (h : Real.cos x₀ ≠ 0) : DifferentiableAt ℝ tan x₀ := by
  conv => enter[2,x]; rw[Real.tan_eq_sin_div_cos]
  fun_prop (disch:=assumption)

@[simp]
theorem deriv_tan' (f : ℝ → ℝ) (hf : DifferentiableAt ℝ f x₀) (h : cos (f x₀) ≠ 0) :
    deriv (fun x => tan (f x)) x₀
    =
    let  y := f x₀
    let dy := deriv f x₀
    dy / cos y ^ 2 := by
  have h' := deriv.comp (h₂ := tan) (h:=f) x₀ (by fun_prop (disch:=assumption)) (by fun_prop)
  unfold Function.comp at h'
  simp_all
  ring

attribute [fun_prop] Differentiable.arctan

@[simp]
theorem deriv_arctan' (x₀ : ℝ) (f : ℝ → ℝ) (hf : DifferentiableAt ℝ f x₀) :
    deriv (fun x => arctan (f x)) x₀
    =
    let y := f x₀
    let dy := deriv f x₀
    dy / (1 + y ^ 2) := by
  have h' := deriv.comp (h₂ := arctan) (h:=f) x₀ (by fun_prop) (by fun_prop)
  simp_all [Function.comp]
  ring

@[simp]
theorem deriv_const_mul' (c : ℝ) : deriv (HMul.hMul c : ℝ → ℝ) = fun _ => c := by
  funext x
  rw[deriv_const_mul c (d:=(fun x  => x)) (hd := by fun_prop)]
  simp

end MissingTheorems

example : deriv (deriv (fun (x:ℝ) ↦ Real.arctan (1 + Real.tan (x^2 + x)))) 0 = (1/2) := by

  have h' : ∀ x, Real.cos x ≠ 0 := sorry
  have h'' : ∀ x, Real.cos x ^ 2 ≠ 0 := by aesop
  have h''' : ∀ x : ℝ, 1 + x ^ 2 ≠ 0 := by intro x; positivity

  eta_expand
  simp (disch:=first | fun_prop (disch:=first | apply h' | apply h'' | apply h''')
                     | apply h' | apply h'' | apply h''')

  norm_num

simp can almost compute the derivatives but there are two issues. Simp can't apply chain rule so you have to formulate all theorems in "chain rule" form, currently not done in mathlib for trigonometric functions. There is also issue with eta expansion and DisrcTree and simp does not always apply the theorem you expect. fun_trans tactic in SciLean deals with these issues and you could just mark deriv_tan and deriv_arctan with fun_trans attribute.

[Patrick Massot]

My question was exactly: how far are we from having fun_trans in Mathlib?

[Eric Wieser]

Arguably those first three results are better proved without fun_prop:

@[fun_prop]
theorem DifferentiableAt.tan (x₀ : ℝ) (h : Real.cos x₀ ≠ 0) : DifferentiableAt ℝ Real.tan x₀ :=
  Real.hasDerivAt_tan h |>.differentiableAt

@[simp]
theorem deriv_tan (f : ℝ → ℝ) (hf : DifferentiableAt ℝ f x₀) (h : cos (f x₀) ≠ 0) :
    deriv (fun x => tan (f x)) x₀
    =
    let y := f x₀; let dy := deriv f x₀; dy / cos y ^ 2 := by
  convert (Real.hasDerivAt_tan h).comp x₀ hf.hasDerivAt |>.deriv using 1
  field_simp -- difference of opinion on the normal form

@[simp]
theorem deriv_arctan' (x₀ : ℝ) (f : ℝ → ℝ) (hf : DifferentiableAt ℝ f x₀) :
    deriv (fun x => arctan (f x)) x₀
    =
    let y := f x₀
    let dy := deriv f x₀
    dy / (1 + y ^ 2) := by
  convert (Real.hasDerivAt_arctan _).comp x₀ hf.hasDerivAt |>.deriv using 1
  field_simp -- difference of opinion on the normal form

[Alex Meiburg]

Is deriv_arctan' not the same as docs#deriv_arctan ? Up to the implictness of arguments?

[Tomas Skrivan]

Patrick Massot said:

My question was exactly: how far are we from having fun_trans in Mathlib?

Not sure, I'm still tweaking it for SciLean and from my experience with fun_prop it gets really painful to develop the tactic once it is in mathlib. You have to recompile the whole mathlib after any change, resynchronize two repos, PRs take forever. Once I feel fun_trans is more or less stable I will move it to mathlib.

[Patrick Massot]

Ok, it’s good to read there is still hope.

[Tomas Skrivan]

Alex Meiburg said:

Is deriv_arctan' not the same as docs#deriv_actan? Up to the implictness of arguments?

Ohh I missed that :) I probably only checked the theorem for tan and assumed it is the same for arctan