## Stream: maths

### Topic: partial functions again

#### Patrick Massot (Sep 04 2018 at 19:31):

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 (Sep 04 2018 at 19:35):

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 (Sep 04 2018 at 20:03):

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 (Sep 04 2018 at 20:05):

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 (Sep 04 2018 at 20:14):

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

#### Patrick Massot (Sep 04 2018 at 20:17):

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 (Sep 04 2018 at 20:24):

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 (Sep 04 2018 at 20:26):

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

#### Kevin Buzzard (Sep 04 2018 at 20:26):

The applied mathematicians were lying to me

#### Mario Carneiro (Sep 04 2018 at 20:27):

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

#### Kevin Buzzard (Sep 04 2018 at 20:27):

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

#### Mario Carneiro (Sep 04 2018 at 20:28):

well, the chain rule was a derivative

#### Kevin Buzzard (Sep 04 2018 at 20:28):

0/0 -- you got lucky :-)

#### Kevin Buzzard (Sep 04 2018 at 20:29):

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 (Sep 04 2018 at 20:29):

we can differentiate polynomials just fine

#### Kenny Lau (Sep 04 2018 at 20:29):

(hey, you teach Galois theory)

#### Mario Carneiro (Sep 04 2018 at 20:30):

not formal derivatives, real derivatives

#### Kevin Buzzard (Sep 04 2018 at 20:30):

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

#### Kevin Buzzard (Sep 04 2018 at 20:31):

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

#### Kevin Buzzard (Sep 04 2018 at 20:32):

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

#### Mario Carneiro (Sep 04 2018 at 20:32):

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

#### Patrick Massot (Sep 04 2018 at 20:38):

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

That is correct

#### Kevin Buzzard (Sep 04 2018 at 20:39):

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

What?

#### Kevin Buzzard (Sep 04 2018 at 20:40):

The product rule is a low-dimensional coincidence

#### Kenny Lau (Sep 04 2018 at 20:41):

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 (Sep 04 2018 at 20:45): 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 (Sep 04 2018 at 20:47):

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 (Sep 04 2018 at 20:47): finally 4 lines #### Chris Hughes (Sep 04 2018 at 20:48): I think you broke the style guidelines with the last one. #### Kenny Lau (Sep 04 2018 at 20:51): 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 (Sep 04 2018 at 20:52):

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 (Sep 04 2018 at 20:54): Kenny this reminds me of Chris Ford's question "differentiate x^10*sin(x) five times" #### Kevin Buzzard (Sep 04 2018 at 20:54): for which my answer was "10 x^9*sin(x) + x^10*cos(x) every time" #### Kevin Buzzard (Sep 04 2018 at 20:54): Why don't you prove the product rule one time instead? #### Mario Carneiro (Sep 04 2018 at 20:55): or prove that the derivative of x^2 is 2x and then prove 2*1=2 #### Kenny Lau (Sep 04 2018 at 21:01): 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 (Sep 04 2018 at 21:05):

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 (Sep 04 2018 at 21:13): 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 (Sep 04 2018 at 21:34):

one of those proofs actually conformed to the guidelines!

#### Kevin Buzzard (Sep 04 2018 at 21:35):

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

#### Kevin Buzzard (Sep 04 2018 at 21:35):

I mean, why is there a list of tactics?

#### Kenny Lau (Sep 04 2018 at 21:36):

because there are two goals

#### Kevin Buzzard (Sep 04 2018 at 21:36):

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

#### Kevin Buzzard (Sep 04 2018 at 21:38):

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


woo!

#### Sebastien Gouezel (Sep 05 2018 at 07:02):

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 (Sep 05 2018 at 07:20):

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

Last updated: May 09 2021 at 10:11 UTC