fderivWithin Confusion

Stream: new members

[Dominic Steinitz]

This typechecks on https://live.lean-lang.org/ so apparently the derivative of f x = x and g x = -x at 0 are equal.

import Mathlib

theorem fderivWithin_congr_of_eq_on_open
  {m n : ℕ}
  (f g : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)) (s : Set (EuclideanSpace ℝ (Fin m)))
  (he : ∀ x ∈ s, f x = g x) :
  ∀ x ∈ s, fderivWithin ℝ f s x = fderivWithin ℝ g s x := by
    intro z hz
    exact fderivWithin_congr he (he z hz)

def f : EuclideanSpace ℝ (Fin 1) -> EuclideanSpace ℝ (Fin 1) := λ x => x
def g : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := λ x => -x
def s : Set (EuclideanSpace ℝ (Fin 1)) := {λ _ : Fin 1 => (0 : ℝ)}

example : (∀ x ∈ s, f x = g x) → ∀ x ∈ s, fderivWithin ℝ f s x = fderivWithin ℝ g s x  := by
  intro h_eq
  apply fderivWithin_congr_of_eq_on_open f g {0} h_eq

[Dominic Steinitz]

(deleted)

[Eric Wieser]

Your example reduces to

import Mathlib

example :
    fderivWithin ℝ (fun x : ℝ => x) {0} 0 = fderivWithin ℝ (fun x => -x) {0} 0  := by
  refine fderivWithin_congr (by simp) (by simp)

right?

[Eric Wieser]

Maybe docs#hasFDerivWithinAt_singleton is of interest here

[Dominic Steinitz]

Maybe - I would say the derivative of a function on singleton is not defined but maybe when I start thinking about connections I will revise my view.

[Kevin Buzzard]

You would probably also say that 1/0 is not defined but in lean it's also 0

[Kevin Buzzard]

We don't have runtime errors in proofs so we have junk values in proofs instead

[Eric Wieser]

Is this one a junk value? Usually the rule is that fderivWithin is junk if HasFDerivWithinAt is false, but that doesn't apply here

[Winston Yin (尹維晨)]

I think it's important to clarify this. The derivative f' of a function f : E → F at a point x : E is defined as any linear map E → F that makes f x - f y - f' (x - y) = o(x - y) hold as y approaches x from every direction. When you use HasFDerivWithinAt, you're saying that this expression holds as y approaches x while remaining in the given set s, which is weaker. For a set s that doesn't include enough of the tangent directions around x, the FDerivWithinAt is still well defined but may not be unique. You can imagine, for example, that x = 0 in ℝ^2, and s is just the axis-1, so the derivative at 0 within s is only specified along axis-1 but is completely arbitrary along axis-2. The predicate UniqueDiffWithinAt guarantees that the derivative at x within s is unique by requiring that s cover enough of the tangent directions. If you now consider the singleton s = {x}, for a function f, the little-o expression holds trivially when you restrict y to approach x while remaining in {x}, for any choice of f'. In particular, f' = 0 is a valid derivative.

@Kevin Buzzard That the derivative of a function within a singleton is well defined is not a case of junk value, but the choice of f' = 0 in docs#hasFDerivWithinAt_singleton is.