has_deriv_at for function defined on open set

Stream: new members

[Golol]

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]

Where did you get that function?

[Mario Carneiro]

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]

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]

okay, so just ignore that then

[Mario Carneiro]

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

[Golol]

ah hmm that would work for now

[Mario Carneiro]

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

[Golol]

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]

welcome to the weird world of dependent type theory

[Mario Carneiro]

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

[Golol]

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]

just use sub_mul

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Yakov Pechersky]

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.