Zulip Chat Archive

Stream: maths

Topic: partial functions again


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 04 2018 at 20:14):

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

view this post on Zulip 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∥

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 20:26):

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

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 20:26):

The applied mathematicians were lying to me

view this post on Zulip Mario Carneiro (Sep 04 2018 at 20:27):

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

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 20:27):

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

view this post on Zulip Mario Carneiro (Sep 04 2018 at 20:28):

well, the chain rule was a derivative

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 20:28):

0/0 -- you got lucky :-)

view this post on Zulip 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!

view this post on Zulip Kenny Lau (Sep 04 2018 at 20:29):

we can differentiate polynomials just fine

view this post on Zulip Kenny Lau (Sep 04 2018 at 20:29):

(hey, you teach Galois theory)

view this post on Zulip Mario Carneiro (Sep 04 2018 at 20:30):

not formal derivatives, real derivatives

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 20:30):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 20:32):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 04 2018 at 20:38):

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

view this post on Zulip Chris Hughes (Sep 04 2018 at 20:38):

That is correct

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 04 2018 at 20:39):

What?

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 20:40):

The product rule is a low-dimensional coincidence

view this post on Zulip Kenny Lau (Sep 04 2018 at 20:41):

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε , ε, , λ 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

view this post on Zulip 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 $ λ ε , ε, , λ 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

view this post on Zulip Kenny Lau (Sep 04 2018 at 20:47):

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε , ε, , λ 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

view this post on Zulip Kenny Lau (Sep 04 2018 at 20:47):

finally 4 lines

view this post on Zulip Chris Hughes (Sep 04 2018 at 20:48):

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

view this post on Zulip Kenny Lau (Sep 04 2018 at 20:51):

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε , ε, , λ 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

view this post on Zulip Kenny Lau (Sep 04 2018 at 20:52):

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε , ε, , λ 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

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 20:54):

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

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 20:54):

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

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 20:54):

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

view this post on Zulip Mario Carneiro (Sep 04 2018 at 20:55):

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

view this post on Zulip Kenny Lau (Sep 04 2018 at 21:01):

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε , ε, , λ 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

view this post on Zulip Kenny Lau (Sep 04 2018 at 21:05):

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε , ε, , λ 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

view this post on Zulip Kenny Lau (Sep 04 2018 at 21:13):

lemma test : has_complex_derivative_at (λ z, z^2) 2 1 :=
tendsto_nhds_of_metric.2 $ λ ε , ε, , λ 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]

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 21:34):

one of those proofs actually conformed to the guidelines!

view this post on Zulip 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]?

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 21:35):

I mean, why is there a list of tactics?

view this post on Zulip Kenny Lau (Sep 04 2018 at 21:36):

because there are two goals

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 21:36):

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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