Zulip Chat Archive

Stream: maths

Topic: has_deriv_at.continuous_on


view this post on Zulip Benjamin Davidson (Apr 18 2021 at 01:52):

I would like to add the following two lemmas (with α, β, 𝕜, and F under appropriate conditions) :

lemma continuous_at.continuous_on {f : α  β} {s : set α} (hcont :  x  s, continuous_at f x) :
  continuous_on f s :=
λ x hx, (hcont x hx).continuous_within_at

lemma has_deriv_at.continuous_on {f f' : 𝕜  F} {s : set 𝕜} (hderiv :  x  s, has_deriv_at f (f' x) x) :
  continuous_on f s :=
λ x hx, (hderiv x hx).continuous_at.continuous_within_at

I know these lemmas are slightly atypical, but I keep on needing them, so I think adding them is worthwhile. Would they make welcome addition?

view this post on Zulip Benjamin Davidson (Apr 18 2021 at 01:52):

A couple of points about the naming:

  • These lemmas don't actually work with dot notation
  • has_deriv_at.continuous_on creates a conflict: One is not able to use continuous_on if the has_deriv_at namespace is open

If I had to rename them, I would use continuous_on_of_continuous_at_forall and continuous_on_of_has_deriv_at_forall, respectively, but those names are far too lengthy for my liking.

view this post on Zulip Patrick Massot (Apr 18 2021 at 10:23):

Do these lemmas actually save keystrokes? They clearly can't work with dot notation since the main assumption hasn't the right shape, whereas their proof allow using dot notation.

view this post on Zulip Mario Carneiro (Apr 18 2021 at 10:39):

To solve the second issue you should use protected on your lemma

view this post on Zulip Benjamin Davidson (Apr 18 2021 at 17:38):

Patrick Massot said:

Do these lemmas actually save keystrokes? They clearly can't work with dot notation since the main assumption hasn't the right shape, whereas their proof allow using dot notation.

Right, this is exactly why I was asking. With their current names they do save keystrokes (especially the second one), but if I had to give them them longer names then they wouldn't be so helpful.

view this post on Zulip Benjamin Davidson (Apr 18 2021 at 17:41):

For example:

has_deriv_at.continuous_on hderiv,
λ x hx, (hderiv x hx).continuous_at.continuous_within_at,

view this post on Zulip Patrick Massot (Apr 18 2021 at 20:20):

You can add that lemma. The real solution should really to have a powerful and fast continuity tactic, but I guess this will wait for Lean4.

view this post on Zulip Benjamin Davidson (Apr 18 2021 at 21:40):

I presume it's not possible to label continuous_on lemmas with continuity?

view this post on Zulip Benjamin Davidson (Apr 18 2021 at 21:41):

I've also been meaning to ask another question that pertains to this; I'll try to post it tonight.

view this post on Zulip Benjamin Davidson (Apr 19 2021 at 04:46):

I've opened #7260

view this post on Zulip Benjamin Davidson (Apr 19 2021 at 06:25):

Benjamin Davidson said:

I've also been meaning to ask another question that pertains to this; I'll try to post it tonight.

Here's my question:
A lot of the integration lemmas I am writing require assumptions about functions being continuous_on. I am wondering: Is it also worth writing versions of these lemmas that assume that the functions are continuous instead? Although continuousis, obviously, a stricter assumption, it is often easier to prove because one can use the continuity tactic directly (no apply continuous.continuous_on or anything similar necessary), and most of the functions with which these lemmas would be used are continuous, anyway.

view this post on Zulip Johan Commelin (Apr 19 2021 at 06:27):

I think it would be easier to patch continuity to check whether the target is continuous_on, and then just apply continuous.continuous_on before trying what it usually does.

view this post on Zulip Johan Commelin (Apr 19 2021 at 06:28):

(Of course it would be even better if continuity could prove actual continuous_on goals (for functions that aren't necessarily globally ctu)

view this post on Zulip Benjamin Davidson (Apr 19 2021 at 06:29):

IIRC continuity currently makes continuous_on goals very complicated (looking)

view this post on Zulip Benjamin Davidson (Apr 19 2021 at 06:30):

Johan Commelin said:

I think it would be easier to patch continuity to check whether the target is continuous_on, and then just apply continuous.continuous_on before trying what it usually does.

How doable is this?

view this post on Zulip Johan Commelin (Apr 19 2021 at 06:31):

I think very doable. But I'm far from an expert on tactic writing.

view this post on Zulip Scott Morrison (Apr 19 2021 at 06:38):

The hard part is actually specifying exactly what behaviour you want. For this sort of stuff, both the basic tools (collecting lemmas by attributes, trying them against a goal in various combinations) and the programming language support (just Lean do blocks, and easy expr inspection and synthesis) are quite good.

view this post on Zulip Scott Morrison (Apr 19 2021 at 06:38):

continuity is in some sense just a variant of the very generic tactic#solve_by_elim, with some additional support for deciding when to use continuous.comp.

view this post on Zulip Scott Morrison (Apr 19 2021 at 06:39):

Reading the code for continuity (and asking about it here as necessary) would probably be very helpful for deciding exactly what you want from a tactic that handles continuous_on.

view this post on Zulip Scott Morrison (Apr 19 2021 at 06:41):

A slightly orthogonal question is whether to just write separate tactics (e.g. for measurable as well), or to build a more generic framework. Either is possible.

view this post on Zulip Benjamin Davidson (Apr 20 2021 at 06:42):

Sorry for the slow reply, I don't have any experience writing tactics so I've been trying to educate myself by reading the webpage and the code for continuity before replying.
My thought would be to have a tactic that applies continuous.continuous_on, succeeding if it succeeds and failing if it fails. continuity can then use that tactic before running its usual course.
I started branch#continuity with my first attempt. It's probably pretty rubbish, and even if it works I'm pretty sure it tries applying continuous.continuous_on in each iteration which should not be necessary.

view this post on Zulip Benjamin Davidson (Apr 21 2021 at 03:40):

Update: It doesn't work

view this post on Zulip Benjamin Davidson (Apr 21 2021 at 04:20):

I'm afraid I am very lost and will need some help figuring this out.

view this post on Zulip Johan Commelin (Apr 21 2021 at 05:57):

Hmm, my idea was to move all the current continuity stuff to continuity', and then the new continuity does

try { apply continuous.continuous_on },
continuity'

view this post on Zulip Benjamin Davidson (Apr 21 2021 at 08:22):

Okay, I can give that a shot.


Last updated: Jun 17 2021 at 16:20 UTC