Stream: new members

Topic: has_deriv_at for function defined on open set

Golol (Oct 21 2020 at 12:56):

So far I could only find variants of has_deriv_at which take as input a function from a normed group or field to a normed group. I want to talk about the differentiability of a function defined on an open subset of \C, i.e.

constant U : set \C
constant h : is_open U
constant f : U -> \C


I suppose I could extend f by zero and then use has_deriv_at, but this doesn't seem like a natural way to do things.
Should I just make a definition kind of like the following?

def has_deriv_open_subset_at (U : set \C) (h : is_open U) (f : U -> \C) (z : U) : Prop
:= has_deriv_at (extend_by_0 f)


Mario Carneiro (Oct 21 2020 at 13:05):

Where did you get that function?

Mario Carneiro (Oct 21 2020 at 13:06):

I tried to push for a derivative on partial functions early on, but the view was that in practice you only ever get total functions (and we try to keep it that way)

Golol (Oct 21 2020 at 13:07):

I want to formalize some basic lemmas in a complex analysis book I have and in this book functions are pretty much always associated with a domain U.

Mario Carneiro (Oct 21 2020 at 13:08):

okay, so just ignore that then

Mario Carneiro (Oct 21 2020 at 13:08):

just use a total function which is only assumed to be reasonable on U

Golol (Oct 21 2020 at 13:08):

ah hmm that would work for now

Mario Carneiro (Oct 21 2020 at 13:09):

we'll just keep pushing the extend_by_0 part off and maybe we'll never need it

Golol (Oct 21 2020 at 13:13):

So I guess just always carry the domain along with the function and try to never do anything which depends on function values outside its domain. Ok that'll work.

Kevin Buzzard (Oct 21 2020 at 13:13):

welcome to the weird world of dependent type theory

Mario Carneiro (Oct 21 2020 at 13:16):

where the one thing you must avoid at all costs is dependent types

Golol (Oct 21 2020 at 15:13):

I am struggling to rewrite Δ x * (x - z) - Δ z * (x - z) into (Δ x - Δ z) * (x - z)  using right_distrib. The problem is that there is a minus and not a plus. What exactly does this notation actually stand for? Is it Δ x * (x - z) + (-1) * Δ z * (x - z)?

Kenny Lau (Oct 21 2020 at 15:14):

just use sub_mul

Bryan Gin-ge Chen (Oct 21 2020 at 15:18):

To see what notation stands for, you can use set_option pp.notation false.

Bryan Gin-ge Chen (Oct 21 2020 at 15:18):

Though often times you'll also need set_option pp.implicit true to make sense of the output.

Yakov Pechersky (Oct 21 2020 at 15:25):

There is probably a lemma that says that the two statements are equal (- and + (-1) *) but only for types that make sense. So for example, this is not true for nat because there is no-1 in nat, and subtraction in nat isn't what you expect.

Last updated: May 10 2021 at 00:31 UTC