## 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