Zulip Chat Archive

Stream: general

Topic: continuous and differentiable on the interior


Yury G. Kudryashov (Feb 25 2022 at 05:39):

A common assumption in complex analysis is that a function is continuous on a set and is differentiable on its interior. In many cases, we apply a theorem with these assumptions to a function that is differentiable on the whole set. Then the application looks like

my_lemma hd.continuous_on (hd.mono interior_subset)

so we have to use hd twice. If we don't have hd in the environment, we need to prove it first instead of doing apply my_lemma, { ... }, { ... }.
Should we introduce a predicate

def name_me (K) (f : E  F) (s : set E) : Prop := continuous_on f s  differentiable_on K f (interior s)

then provide dot notation lemmas like differentiable_on.name_me? If yes, what name would you suggest?

Yury G. Kudryashov (Feb 25 2022 at 06:07):

Let me suggest cont_diff_on_int. Better names are welcome.

Sebastien Gouezel (Feb 25 2022 at 06:47):

I'd rather avoid anything containing cont_diff, because in mathlib this now relates to higher smoothness. diff_on_int_cont would be ok, though.

Yury G. Kudryashov (Feb 25 2022 at 07:03):

OK.

Yury G. Kudryashov (Mar 26 2022 at 03:47):

Now I wonder which notion is more useful: diff_on_int_cont or diff_cont_on_cl K f s := differentiable_on K f s ∧ continuous_on f (closure s)? The latter takes an open domain as an argument.


Last updated: Dec 20 2023 at 11:08 UTC