has_deriv_at.continuous_on

Stream: maths

[Benjamin Davidson]

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?

[Benjamin Davidson]

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.

[Patrick Massot]

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.

[Mario Carneiro]

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

[Benjamin Davidson]

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.

[Benjamin Davidson]

For example:

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

[Patrick Massot]

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.

[Benjamin Davidson]

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

[Benjamin Davidson]

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

[Benjamin Davidson]

I've opened #7260

[Benjamin Davidson]

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.

[Johan Commelin]

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.

[Johan Commelin]

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

[Benjamin Davidson]

IIRC continuity currently makes continuous_on goals very complicated (looking)

[Benjamin Davidson]

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?

[Johan Commelin]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Scott Morrison]

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.

[Scott Morrison]

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.

[Benjamin Davidson]

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.

[Benjamin Davidson]

Update: It doesn't work

[Benjamin Davidson]

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

[Johan Commelin]

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'

[Benjamin Davidson]

Okay, I can give that a shot.