## Stream: new members

### Topic: piecewise functions

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


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

#### Reid Barton (Dec 20 2018 at 06:19):

There's also continuous_if and continuous_subtype_is_closed_cover

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

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

#### Kenny Lau (Dec 20 2018 at 07:19):

@Patrick Massot merciless

#### Johan Commelin (Dec 20 2018 at 07:41):

Completely agree. Let's get these PRs moving.

#### Aymon Wuolanne (Dec 20 2018 at 07:56):

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

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

#### Johan Commelin (Dec 20 2018 at 07:58):

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

#### Mario Carneiro (Dec 20 2018 at 07:58):

I thought frontier was closure s \ s

#### Johan Commelin (Dec 20 2018 at 07:59):

So what is s \ interior s called?

#### Reid Barton (Dec 20 2018 at 07:59):

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

#### Reid Barton (Dec 20 2018 at 07:59):

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

#### Mario Carneiro (Dec 20 2018 at 08:00):

So what is s \ interior s called?

outliers?

#### Johan Commelin (Dec 20 2018 at 08:00):

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

#### Mario Carneiro (Dec 20 2018 at 08:01):

periphery is nice

#### Johan Commelin (Dec 20 2018 at 08:01):

is borderline acceptable

#### Mario Carneiro (Dec 20 2018 at 08:01):

it's borderline acceptable

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

#### Mario Carneiro (Dec 20 2018 at 08:02):

boundary is useful though

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

#### Mario Carneiro (Dec 20 2018 at 20:45):

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

#### Patrick Massot (Dec 20 2018 at 20:50):

Would you give this PR a master's thesis?

#### Callum Cassidy-Nolan (Mar 04 2022 at 16:28):

I managed to write a piecewise function like this: (h : g = λ x, if x < 2 then 2 * x else 2^x), is there a cleaner way to deal with more complicated piecewise functions? Like this : image.png

#### Alex J. Best (Mar 04 2022 at 16:31):

I'd probably just do it with two ifs, that seems reasonable, the tactic#split_ifs should make unpacking them into 3 goals fairly painless

#### Callum Cassidy-Nolan (Mar 04 2022 at 16:37):

Yeah I'll go with that method, another question I have is why if I change it to :  (h : g = λ x, if x ∈ set.Iio (2 : ℝ) then 2 * x else 2^x)  then I get

failed to synthesize type class instance for
g : ℝ → ℝ,
x : ℝ
⊢ decidable (x ∈ set.Iio 2)


#### Kevin Buzzard (Mar 04 2022 at 16:40):

Put open_locale classical at the top of your file

#### Callum Cassidy-Nolan (Mar 04 2022 at 16:50):

How would we deal with piecewise functions like this: image.png (there is a hole at (0,1)

#### Callum Cassidy-Nolan (Mar 04 2022 at 16:51):

it's x^2 + 1 on the left and x + 1 on the right

#### Alex J. Best (Mar 04 2022 at 16:57):

In lean all functions are total, so you would have to define the function on the domain {x : real // x \ne 0} to represent a hole, or use docs#option for the missing point.

#### Callum Cassidy-Nolan (Mar 04 2022 at 17:02):

Oh ok, are there docs on how the if else blocks work? I want to do an else if and leave of the else block but I'm not sure if that's possible

it's not

#### Mario Carneiro (Mar 04 2022 at 17:03):

the if syntax is if p then a else b

#### Mario Carneiro (Mar 04 2022 at 17:03):

or if h : p then a else b

#### Mario Carneiro (Mar 04 2022 at 17:04):

it doesn't really make sense to leave the else block off in most cases

#### Callum Cassidy-Nolan (Mar 04 2022 at 17:04):

I was interested in that because I only wanted to define the function for a certain interval

#### Mario Carneiro (Mar 04 2022 at 17:04):

you need a domain constraint if you want to make the function undefined

#### Mario Carneiro (Mar 04 2022 at 17:05):

like a hypothesis (h : x != 2)

#### Mario Carneiro (Mar 04 2022 at 17:05):

or you can return an option

#### Mario Carneiro (Mar 04 2022 at 17:05):

or you can return a garbage value (this is what we usually do)

#### Callum Cassidy-Nolan (Mar 04 2022 at 17:10):


Mario Carneiro said:

like a hypothesis (h : x != 2)

Where would this hypothesis go? Would it be part of the lambda ? λ x (h : x ≠ 0), ...

#### Callum Cassidy-Nolan (Mar 04 2022 at 17:14):

Mario Carneiro said:

or you can return a garbage value (this is what we usually do)

You're suggesting something like

    (h₀ : h = λ x, if x < 0 then x^2 + 1 else x + 1 )
(h₁ : h 0 = 999)


?

#### Kevin Buzzard (Mar 04 2022 at 17:15):

Right now we are asking you to decide the domain and codomain of your function

#### Kevin Buzzard (Mar 04 2022 at 17:17):

A function goes from an input type to an output type. You have given us a picture which is all very nice but what are your input type and output type. Remember that a function has to be defined at every value of the input type and give an answer in the output type

#### Kevin Buzzard (Mar 04 2022 at 17:18):

Before we can define the term (the function) we need to know the type of the term (X -> Y)

#### Callum Cassidy-Nolan (Mar 04 2022 at 17:36):

Ah ok, I think I get the just of it, if I make it R -> R then we use a garage value, because as you said the function needs to be defined at every place

#### Callum Cassidy-Nolan (Mar 04 2022 at 17:37):

What about piecewise functions that are like this? :
image.png

#### Mario Carneiro (Mar 04 2022 at 17:39):

that's a specification, not a definition. How do you even know that the function is well defined?

#### Callum Cassidy-Nolan (Mar 04 2022 at 17:41):

It was specified as a function,  (h : f = λ n, if 1000 ≤ n then n - 3 else f (f (n + 5)) seems to work fine, but for some reason I thought we would have to use the inductive type

#### Mario Carneiro (Mar 04 2022 at 17:43):

Taking that as an assumption is saying that you assume f` is a function satisfying the specification

#### Mario Carneiro (Mar 04 2022 at 17:43):

it does not prove the existence of such a function

#### Kevin Buzzard (Mar 04 2022 at 18:33):

That definition shouldn't "work fine", there are things to be proved before you can talk about f, i.e. that there exists a unique function with that property.

Last updated: Dec 20 2023 at 11:08 UTC