Zulip Chat Archive

Stream: new members

Topic: piecewise functions


view this post on Zulip Aymon Wuolanne (Dec 20 2018 at 04:10):

Does anyone have any tips for dealing with piecewise functions, in particular showing that they're continuous? I have something like the following in mind:

variables (a : ℝ) (f : ℝ → ℝ) (g : ℝ → ℝ)
def pw : ℝ → ℝ := λ x, if x ≤ a then f x else g x
lemma continuous_pw : continuous f → continuous g → f a = g a → continuous (pw a f g) := sorry

view this post on Zulip Jeremy Avigad (Dec 20 2018 at 05:00):

Coincidentally, I just issued a pull request with some additions to the analysis library. There is a lemma called tendsto_if which will be helpful: https://github.com/avigad/mathlib/blob/limit_stuff/order/filter.lean#L1257-L1261. I'd use the fact that a function is continuous if it is continuous at every point (which used to be called continuous_iff_tendsto but in my PR is continuous_iff_continuous_at. Using metric_space you can unwrap the definition of neighborhoods in terms of distance.

view this post on Zulip Reid Barton (Dec 20 2018 at 06:19):

There's also continuous_if and continuous_subtype_is_closed_cover

view this post on Zulip Patrick Massot (Dec 20 2018 at 07:16):

Coincidentally, I just issued a pull request with some additions to the analysis library.

You should expect a lot of homework now, that Mario guy is merciless...

view this post on Zulip Patrick Massot (Dec 20 2018 at 07:18):

Seriously I'm very excited to see some PR from your analysis work. I hope you already discussed it enough with Mario, and will convince Johannes quickly. It would be very nice to have a topology PR merge sprint before Amsterdam (or even before Christmas, and then a second one before Amsterdam)

view this post on Zulip Kenny Lau (Dec 20 2018 at 07:19):

@Patrick Massot merciless

view this post on Zulip Johan Commelin (Dec 20 2018 at 07:41):

Completely agree. Let's get these PRs moving.

view this post on Zulip Aymon Wuolanne (Dec 20 2018 at 07:56):

Thanks! I think I should be able to get it working with continuous_if

view this post on Zulip Aymon Wuolanne (Dec 20 2018 at 07:57):

Side note: frontier is defined as closure s \ interior s, isn't this usually referred to as the boundary?

view this post on Zulip Johan Commelin (Dec 20 2018 at 07:58):

I've never heard of frontier before. I learned it as boundary.

view this post on Zulip Mario Carneiro (Dec 20 2018 at 07:58):

I thought frontier was closure s \ s

view this post on Zulip Johan Commelin (Dec 20 2018 at 07:59):

So what is s \ interior s called?

view this post on Zulip Reid Barton (Dec 20 2018 at 07:59):

apparently it is sometimes called the boundary! not even making this up

view this post on Zulip Reid Barton (Dec 20 2018 at 07:59):

https://en.wikipedia.org/wiki/Boundary_(topology)

view this post on Zulip Mario Carneiro (Dec 20 2018 at 08:00):

So what is s \ interior s called?

outliers?

view this post on Zulip Johan Commelin (Dec 20 2018 at 08:00):

https://www.thesaurus.com/browse/boundary enough words to choose from (-;

view this post on Zulip Mario Carneiro (Dec 20 2018 at 08:01):

periphery is nice

view this post on Zulip Johan Commelin (Dec 20 2018 at 08:01):

is borderline acceptable

view this post on Zulip Mario Carneiro (Dec 20 2018 at 08:01):

it's borderline acceptable

view this post on Zulip Mario Carneiro (Dec 20 2018 at 08:02):

but actually I find very little use for these concepts, they are more a historical note for me

view this post on Zulip Mario Carneiro (Dec 20 2018 at 08:02):

boundary is useful though

view this post on Zulip Jeremy Avigad (Dec 20 2018 at 20:38):

Mario has gone easy on me so far. I am about to get on a flight to California to visit my in-laws, but I should be able to make the corrections there.

view this post on Zulip Mario Carneiro (Dec 20 2018 at 20:45):

It looks pretty good. there is absolutely no chance of a conflict of interest, yep

view this post on Zulip Patrick Massot (Dec 20 2018 at 20:50):

Would you give this PR a master's thesis?


Last updated: May 13 2021 at 22:15 UTC