piecewise functions

Stream: new members

[Aymon Wuolanne]

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]

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]

There's also continuous_if and continuous_subtype_is_closed_cover

[Patrick Massot]

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]

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]

@Patrick Massot merciless

[Johan Commelin]

Completely agree. Let's get these PRs moving.

[Aymon Wuolanne]

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

[Aymon Wuolanne]

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

[Johan Commelin]

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

[Mario Carneiro]

I thought frontier was closure s \ s

[Johan Commelin]

So what is s \ interior s called?

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

So what is s \ interior s called?

outliers?

[Johan Commelin]

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

[Mario Carneiro]

periphery is nice

[Johan Commelin]

is borderline acceptable

[Mario Carneiro]

it's borderline acceptable

[Mario Carneiro]

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

[Mario Carneiro]

boundary is useful though

[Jeremy Avigad]

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]

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

[Patrick Massot]

Would you give this PR a master's thesis?

[Callum Cassidy-Nolan]

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]

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]

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]

Put open_locale classical at the top of your file

[Callum Cassidy-Nolan]

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

[Callum Cassidy-Nolan]

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

[Alex J. Best]

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]

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

[Mario Carneiro]

it's not

[Mario Carneiro]

the if syntax is if p then a else b

[Mario Carneiro]

or if h : p then a else b

[Mario Carneiro]

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

[Callum Cassidy-Nolan]

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

[Mario Carneiro]

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

[Mario Carneiro]

like a hypothesis (h : x != 2)

[Mario Carneiro]

or you can return an option

[Mario Carneiro]

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

[Callum Cassidy-Nolan]

`
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]

Mario Carneiro said:

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

So for this example : https://leanprover.zulipchat.com/user_uploads/3121/Ybk2YpR0VKpVsRv8PPps8UfU/image.png

You're suggesting something like

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

?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Callum Cassidy-Nolan]

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]

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

[Mario Carneiro]

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

[Callum Cassidy-Nolan]

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]

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

[Mario Carneiro]

it does not prove the existence of such a function

[Kevin Buzzard]

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.