partial functions again

Stream: maths

[Patrick Massot]

With the recent merges from my so-called differential topology repository to mathlib, the next target in this direction is the definition of derivatives (Fréchet derivative if you insist on this terminology). It is very easy to say that a function defined on a whole normed vector space is differentiable at some point a: https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/calculus.lean#L17 But of course we want derivatives of functions defined on a subset of a normed space, at least allowing an open set. I can clearly try to adapt the definition, but I'd be happy to read any advice.

[Patrick Massot]

For instance, https://github.com/thalesant/formalabstracts/blob/riemann_hypothesis/folklore/complex.lean#L227 (in the holomorphic case, but this doesn't matter) define a function from a subset of a normed space to be differentiable at x if the subset is open and the extension by zero (which is defined everywhere) is differentiable at x. This is one option

[Patrick Massot]

I ran a quick sanity check on the definition from FAbstract (I wanted to see with my own eyes that division by zero works as intended).

import analysis.complex
import analysis.limits

open filter complex

def has_complex_derivative_at
(f : ℂ → ℂ)
(f'z : ℂ)
(z : ℂ) : Prop :=
let error_term (h : ℂ) : ℝ :=
    abs((f (z + h) - (f z + f'z * h))/h) in
(tendsto error_term (nhds (0 : ℂ)) (nhds (0:ℝ)))

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
begin
  dsimp only [has_complex_derivative_at],

  have :  (λ h : ℂ, abs (((1 + h) ^ 2 - (1 ^ 2 + 2 * h))/h)) = (λ h, abs(h^2/h)),
  by ext ; congr; ring,
  rw this,

  rw tendsto_nhds_of_metric,
  intros ε ε_pos,
  existsi [ε, ε_pos],
  intros x dx,
  by_cases h : x = 0,
  { simpa [h, ε_pos] },
  { rw [pow_two, mul_div_cancel x h],
    dsimp[dist] at dx ⊢,
    simpa using dx }
end

[Patrick Massot]

First I'm both amazed and ashamed that I wrote that so quickly without insulting my computer. But of course I'd be very happy to read a simpler proof. @Rob Lewis please feel free to explain that your Lean/Sage bridge allows to do this limit computation in one line.

[Patrick Massot]

I can merge the last two lines in simpa [dist] using dx

[Patrick Massot]

Anyway, this great success of division by zero makes me wonder whether I should define differentiability using ∥f (a + h) - f a - L h∥/ ∥h∥

[Chris Hughes]

Golfed as requested

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
have (λ h : ℂ, abs (((1 + h) ^ 2 - (1 ^ 2 + 2 * h)) / h)) = (λ h, abs (h ^ 2 / h)),
  by ext; congr; ring,
by simp only [has_complex_derivative_at, this, tendsto_nhds_of_metric];
  exact λ ε ε0, ⟨ε, ε0, λ x dx, if h : x = 0 then by simpa [h, ε0]
  else by dsimp [dist] at *; simpa [pow_two, mul_div_cancel x h] using dx⟩

[Kevin Buzzard]

So 0/0 isn't 1? ;-)

[Kevin Buzzard]

The applied mathematicians were lying to me

[Mario Carneiro]

0/0 = 0 is actually really convenient for stating the definition of the derivative

[Kevin Buzzard]

PS are we witnessing the first time Lean has ever differentiated a function here?

[Mario Carneiro]

well, the chain rule was a derivative

[Kevin Buzzard]

0/0 -- you got lucky :-)

[Kevin Buzzard]

Chris -- with the binomial theorem you can differentiate x^n and with Patrick's knowledge of filters he can prove differentiation is linear, and then we can differentiate polynomials!

[Kenny Lau]

we can differentiate polynomials just fine

[Kenny Lau]

(hey, you teach Galois theory)

[Mario Carneiro]

not formal derivatives, real derivatives

[Kevin Buzzard]

But of course we need to differentiate cos too :-)

[Kevin Buzzard]

That will follow from C-linearity if someone can differentiate exp. Mario did you say there was a dirty trick for that?

[Kevin Buzzard]

I guess step one is to get exp in mathlib...

[Mario Carneiro]

yes, 1 + x <= exp x <= 1/(1-x) proves exp' 0 = 1 and then it's easy

[Patrick Massot]

Thanks Chris. I think it's exactly the same proof though.

[Chris Hughes]

That is correct

[Kevin Buzzard]

It's easy if you have the product rule, but Patrick doesn't believe in the product rule

[Patrick Massot]

What?

[Kevin Buzzard]

The product rule is a low-dimensional coincidence

[Kenny Lau]

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z hz,
if h : z = 0 then by simpa [h] else
by simp [pow_two, mul_add, add_mul, two_mul, dist];
rw [← complex.abs_mul z, ← complex.abs_div, mul_div_cancel _ h];
simpa [dist] using hz⟩

[Kenny Lau]

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
have H : ∀ z : ℂ, -1 + (-(2 * z) + (z + 1) ^ 2) = z * z,
  from λ _, by ring,
tendsto_nhds_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z hz,
if h : z = 0 then by simpa [h] else
by simp [H, mul_div_cancel _ h, -complex.abs_div];
simpa [dist] using hz⟩

[Kenny Lau]

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z hz,
if h : z = 0 then by simpa [h] else by simp [pow_two,
mul_add, add_mul, two_mul, mul_div_cancel _ h,
-complex.abs_div]; simpa [dist] using hz⟩

[Kenny Lau]

finally 4 lines

[Chris Hughes]

I think you broke the style guidelines with the last one.

[Kenny Lau]

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z hz,
if h : z = 0 then by simpa [h] else
by simp [pow_two, add_mul_self_eq, mul_div_cancel _ h, -complex.abs_div];
simpa [dist] using hz⟩

[Kenny Lau]

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z hz,
if h : z = 0 then by simpa [h] else
by simp [pow_two, add_mul_self_eq, -complex.abs_div];
simpa [mul_div_cancel _ h, dist] using hz⟩

[Kevin Buzzard]

Kenny this reminds me of Chris Ford's question "differentiate x^10*sin(x) five times"

[Kevin Buzzard]

for which my answer was "10 x^9*sin(x) + x^10*cos(x) every time"

[Kevin Buzzard]

Why don't you prove the product rule one time instead?

[Mario Carneiro]

or prove that the derivative of x^2 is 2x and then prove 2*1=2

[Kenny Lau]

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z hz,
if h : z = 0 then by simpa [h] else trans_rel_right _
(by simp [dist, pow_two, add_mul_self_eq, mul_div_cancel _ h, -complex.abs_div]) hz⟩

[Kenny Lau]

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z hz,
if h : z = 0 then by simpa [h] else by dsimp; rw [pow_two];
by simpa [dist, add_mul_self_eq, mul_div_cancel _ h, -complex.abs_div] using hz⟩

[Kenny Lau]

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z hz,
by simp [pow_two, add_mul_self_eq, dist, -complex.abs_div] at *;
by_cases h : z = 0; [simpa [h], rwa mul_div_cancel _ h]⟩

[Kevin Buzzard]

one of those proofs actually conformed to the guidelines!

[Kevin Buzzard]

I don't understand the last one. What is this [simpa [h], rwa mul_div_cancel _ h]?

[Kevin Buzzard]

I mean, why is there a list of tactics?

[Kenny Lau]

because there are two goals

[Kevin Buzzard]

oh! The n'th term in the list acts on the n'th goal?

[Kevin Buzzard]

example (p q : Prop) (hp : p) (hq : q) : p ∧ q :=
begin
  split;[exact hp,exact hq]
end

woo!

[Sebastien Gouezel]

If you want to define differentiability in a rather broad setting, you certainly want it to contain differentiability on the left and on the right for 1-dimensional functions, and differentiability on manifolds with boundaries. The best setting for this is probably differentiability in the sense of Whitney, i.e., f is differentiable at x on S if there is a linear operator such that f(y)-f(x) -L (y-x)/ ||y-x|| tends to 0 when ytends to xwhile remaining in S. This is certainly easy to define if you have a filter like nhbds_within (defined using nhbds x and principal S and the good filter operation (I never know in which direction they go)). This filter would also be useful to define continuity within S, as far as I can tell this is not in Lean?.

With the big warning that the differential is not unique in general, if the tangent directions of S at x do not span the whole subspace. For uniquenss statement, you would probably want that S is a neighborhood of x, say.

[Johannes Hölzl]

the good filter operation is infimum: nhds_within a s := nhds a ⊓ principal s