Derivative of an Inverse

Stream: new members

[Colin Jones ⚛️]

I'm having difficulty proving this statement:

import Mathlib

example (y : ℝ) (hy : 0 < y) : deriv (fun x => (x ^ 2)⁻¹) y = - 2 * (1 / y) := by
  sorry

Especially since I can't transform the interior into a good form e.g.

example (x : ℝ) (hx : 0 < x) : (x ^ (2:ℝ))⁻¹ = x ^ (-2 : ℝ) := Eq.symm (Real.rpow_neg (le_of_lt hx) 2)

I can't get this to work because I don't know how to let Lean know that the function will never have an input of 0.

[Eric Wieser]

Your goal is false

[Eric Wieser]

But here's how you can get there:

import Mathlib

example (y : ℝ) (hy : 0 < y) : deriv (fun x => (x ^ 2)⁻¹) y = - 2 * (1 / y) := by
  -- the `_` in the statement lets Lean build it for us
  have : HasDerivAt (fun x => (x ^ 2)⁻¹) _ y
  · refine HasDerivAt.inv (HasDerivAt.pow _ (hasDerivAt_id' _)) ?_
    positivity
  have := this.deriv
  rw [this]
  field_simp [hy.ne]
  ring
  -- oops

[Eric Wieser]

@Kyle Miller, do you know if it's possible to write the above using a core-style have?

[Edward van de Meent]

you're missing a ^3 on the rhs

[Colin Jones ⚛️]

Oh yep my bad.

[Yury G. Kudryashov]

See also docs#deriv_zpow

[Colin Jones ⚛️]

This is a better example. I had to transform the types around and mess with the proof statement

example : deriv (fun x => x ^ (-1:ℤ)) x = - x ^ (-2:ℤ) := by
  rw [show - x ^ (-2:ℤ) = (-1:ℤ) * x ^ (-2:ℤ) by ring, show (-2 : ℤ) = -1 - 1 by ring]
  apply deriv_zpow (-1:ℤ)

[Colin Jones ⚛️]

Here's an answer to my original question.

example (hx : x ≠ 0) : deriv (fun x => x ^ (-2 : ℝ)) x = (-2) * x ^ (-3 : ℝ) := by
  rw [show (-3 : ℝ) = -2 - 1 by ring]
  refine Real.deriv_rpow_const (by left; assumption)

[Notification Bot]

Colin Jones ⚛️ has marked this topic as resolved.

[Notification Bot]

Colin Jones ⚛️ has marked this topic as unresolved.

[Colin Jones ⚛️]

example (hx : y ≠ 0) : deriv (fun x => 1 / x ^ (2 : ℝ)) y = -2 * x ^ (-3 : ℝ) := by
  rw [show (-3:ℝ) = -2 - 1 by ring]
  simp_rw [show (fun x => 1 / x ^ 2) = (fun x => x ^ (-2:ℝ)) by funext]

I still can't convert the rational to the condensed exponent form.

[Yury G. Kudryashov]

Where did you get this problem from?

[Kyle Miller]

@Eric Wieser It looks like you can do

  have : HasDerivAt (fun x => (x ^ 2)⁻¹) _ y :=
    HasDerivAt.inv (HasDerivAt.pow _ (hasDerivAt_id' _)) (by positivity)

It's times like this where I wish there were another class of metavariable, "intentional natural metavariables". This fails because the first ?_ is not assignable during unification in the elaborator:

  have : HasDerivAt (fun x => (x ^ 2)⁻¹) ?_ y := by
    refine HasDerivAt.inv (HasDerivAt.pow _ (hasDerivAt_id' _)) ?_
    positivity

[Kyle Miller]

Hmm, there's a hack to disable the stricter metavariable check, but I wouldn't count on this being a feature:

  have : HasDerivAt (fun x => (x ^ 2)⁻¹) _ y := id <| by
    refine HasDerivAt.inv (HasDerivAt.pow _ (hasDerivAt_id' _)) ?_
    positivity

[Eric Wieser]

Could we build that hack into have so that it can be relied upon?

[Kyle Miller]

It'd be good to have an issue collecting a couple examples of using have to build up terms like HasDerivAt. This is a good example of one of the arguments being an 'output' that you intend to compute.

Here's a more reliable hack, but still a hack:

  have : ?_ := by
    refine (?_ : HasDerivAt (fun x => (x ^ 2)⁻¹) _ y)
    refine HasDerivAt.inv (HasDerivAt.pow _ (hasDerivAt_id' _)) ?_
    positivity

[Tyler Josephson ⚛️]

Yury G. Kudryashov said:

Where did you get this problem from?

I’m pretty sure this is a #mwe version of a proof about the derivative of the LJ potential https://en.m.wikipedia.org/wiki/Lennard-Jones_potential, relating energy and force, as we’re building code for formally-verified molecular dynamics.

[Kevin Buzzard]

Why are you raising things to real powers rather than natural or integer powers? Why not just stick to naturals or integers?

[Colin Jones ⚛️]

For consistency

[Tyler Josephson ⚛️]

Kevin Buzzard said:

Why are you raising things to real powers rather than natural or integer powers? Why not just stick to naturals or integers?

In science and engineering applications, I think we need rational powers, for example, sometimes we need to represent 3/2 power, or an empirically-measured power with a fixed amount of precision. I can’t think of a case when we’d have an irrational power, like pi, e, or sqrt(2).

[Yury G. Kudryashov]

Note that (-8 : Real) ^ (1 / 3 : Real) = 1 in Mathlib. I have plans to redefine docs#Real.rpow so that it gives the "right" answer -2 in this case but this isn't my top priority.

[Yury G. Kudryashov]

(x : Real) ^ (y : Real) has meaningful value (in today's Mathlib) only for x ≥ 0.

[Eric Wieser]

#7907 is somewhat related here too

[Yury G. Kudryashov]

I think that we should separate the "new notation" PR and the "new definition" PR.