Junk values in differentiation

Stream: Lean for Scientists and Engineers 2024

[Tyler Josephson ⚛️]

Here's a curious function (visualized here)
f(x) = (x^2)/(x -1)

It has a local maximum and a local minimum at x = 0 and x = 2, respectively (i.e., df/dx = 0). At x = 1, the derivative doesn't exist (since divide by 0), so according to deriv, df/dx = 0 here, as well (as a junk value).

This might be an interesting problem setup for someone interested in digging into how the junk value 0 interacts with the actual derivative=0 maximum and minimum. If you work out something neat, I'd love to see it, and would include that example in next year's class!

[Eric Wieser]

Here's all but the final piece:

import Mathlib

example : deriv (fun x : ℝ => x^2/(x - 1)) =
    fun x => (x - 2)*x/(x-1)^2 := by
  ext x
  obtain rfl | hx := eq_or_ne x 1
  · rw [deriv_zero_of_not_differentiableAt, sub_self, zero_pow two_ne_zero, div_zero]
    show ¬DifferentiableAt ℝ (fun x => x ^ 2 / (x - 1)) 1
    sorry
  · have : HasDerivAt (fun x => x^2/(x - 1)) _ x :=
      .div (.pow 2 (hasDerivAt_id' _)) (.sub (hasDerivAt_id' _) (hasDerivAt_const _ _)) ?_
    · convert this.deriv using 1
      ring_nf
    · rwa [sub_ne_zero]

[Adomas Baliuka]

The hole will be easiest to prove once https://github.com/leanprover-community/mathlib4/pull/15200#issue-2433523881 is merged