Zulip Chat Archive

Stream: Lean Together 2019

Topic: analysis session


view this post on Zulip Jeremy Avigad (Jan 09 2019 at 13:59):

Friends,

I am planning to formalize derivatives, etc. in terms of Lean's partial function type. To that end, I have generalized limits to partial functions (and even partial multifunctions = relations). I told Rob and Johannes that I'd like to talk about that in the analysis session, because I can use some feedback. In response, they told me I could moderate the session and abuse my status as moderator to talk about whatever I want. That works for me.

It would also be helpful to me to hear about Cyril's experiences formalizing analysis in Coq. So here is what I am thinking about for the session:

(1) a quick overview of approaches to dealing with partial functions (me, <= 15 minutes)

(2) notions of limits for partial functions and relations (e.g. what lim_{x -> a} f(x) means when f is partial) (me, <= 15 minutes)

(3) an overview of analysis in Coq (Cyril, ~20 minutes)

My thought is that I can mostly defer questions in (1) and (2), and then after Cyril has a chance to talk to a while, we can turn the session into open discussion. Does anyone object to that plan?

view this post on Zulip Joseph Corneli (Jan 15 2019 at 14:48):

I know Jeremy said he didn't want to start a debate about which way of representing partial functions is "better" but maybe it's worth sharing an after-the-fact reflection about how very different two of the options are.

Let's start with the indicator function:

χ[0,1]:RR\chi_{[0,1]}\colon \mathbb{R}\rightarrow\mathbb{R},
x[0,1]χ(x)=1x\in[0,1]\Rightarrow\chi(x)=1, x[0,1]χ(x)=0x\notin[0,1]\Rightarrow \chi(x)=0

If we were to talk about a function ψ:RR\psi\colon\mathbb{R}\rightarrow\mathbb{R} with the property ψ[0,1]=χ[0,1]\psi\vert_{[0,1]}=\chi_{[0,1]}, it seems to me that, until we are given further information, the values of ψ\psi outside of [0,1][0,1] are more comfortably thought of as unknown, or even irrelevant, but not wholly "undefined". In particular, we know that these values are in R\mathbb{R}.

So in the spirit of the example, we could define a "partial function on R\mathbb{R} that is equal to 11 on [0,1][0,1]" to be the set of all functions on R\mathbb{R} that are equal to 11 on [0,1][0,1]. Actually, this seems to just be the "relation" option that Jeremy described, indeed, equality-on-the-unit-interval looks to be an equivalence relation. Well, I admit, I do have a bias, which is that this definition seems to capture something "geometric" that the definition using undefined doesn't (at least not so directly).

view this post on Zulip Patrick Massot (Jan 15 2019 at 14:52):

I still think this is a very bad example, since the indicator function is a total function, without any discussion. Its values outside [0,1][0, 1] are not undefined in any sense

view this post on Zulip Joseph Corneli (Jan 15 2019 at 14:53):

But you could make an information-theoretic version of the indicator function that masks all information outside of the unit interval.

view this post on Zulip Patrick Massot (Jan 15 2019 at 14:54):

For instance, it is of utmost importance that, for every other (say continuous) function ff , [0,1]f=Rfχ[0,1]\int_{[0, 1]} f = \int_\mathbb{R} f\chi_{[0, 1]}. There is no other value than zero that would make that true

view this post on Zulip Mario Carneiro (Jan 15 2019 at 14:54):

This assumes the codomain is inhabited, else that set might be empty

view this post on Zulip Mario Carneiro (Jan 15 2019 at 14:55):

in general it shares many of the downsides of things like continuous extensions - they may not exist, although it's nice when they do

view this post on Zulip Patrick Massot (Jan 15 2019 at 14:56):

Mario, what are "This" and "it" in your latest messages?

view this post on Zulip Mario Carneiro (Jan 15 2019 at 14:56):

in short, taking a quotient will not mask all information; you are left with trunc

view this post on Zulip Mario Carneiro (Jan 15 2019 at 14:56):

this procedure of using sets of functions extending a partial function to represent partial functions

view this post on Zulip Patrick Massot (Jan 15 2019 at 14:57):

ok

view this post on Zulip Mario Carneiro (Jan 15 2019 at 14:58):

the type that does mask all information when the predicate is false is roption, and corresponds to the data.pfun implementation of partial functions

view this post on Zulip Joseph Corneli (Jan 15 2019 at 15:03):

@Mario Carneiro an interesting example is tangent, which is defined, after all, as a quotient in the function sense. It also "tiles" so looks like a quotient in a geometric sense. I realise many other cases won't have the same feel or origin story but it seems like the partiality in this case emerges from a process.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 15:04):

I don't follow. The tangent function is not a partial function, unless you are talking about behavior at the poles

view this post on Zulip Joseph Corneli (Jan 15 2019 at 15:04):

Yes, that's what I'm talking about.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 15:05):

I don't see how saying "tan (pi/2) is a real number but we don't know which" is a satisfying solution

view this post on Zulip Joseph Corneli (Jan 15 2019 at 15:06):

Well, it's not a real number but what is it?

view this post on Zulip Johan Commelin (Jan 15 2019 at 15:07):

It is 37, or 0, depending on whom you are asking.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 15:07):

Again I think that roption really is capturing the right idea. It's isomorphic to the class of subsets of R with at most one element

view this post on Zulip Mario Carneiro (Jan 15 2019 at 15:07):

and this allows you to actually say "tan (pi/2) is not a real number"

view this post on Zulip Mario Carneiro (Jan 15 2019 at 15:08):

it induces a relation "r is the tan of x" which is satisfied for no r at pi/2

view this post on Zulip Joseph Corneli (Jan 15 2019 at 15:09):

All this does seem good but I feel I'd want to see this emerging as a "limit" of some kind.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 15:10):

the limit comes in the fact that to define an roption you need a predicate, and this predicate describes the good behavior of the object, be it a limit, or multiplying to something reasonable, etc. If no such element exists then the value is undefined

view this post on Zulip Mario Carneiro (Jan 15 2019 at 15:13):

In general, I don't think we want to give any additional structure to generic partial functions; just like how functions are arbitrary maps not continuous maps or other things, partial functions can have any domain, not just open domains, and the mapping may not be computable or anything else like that

view this post on Zulip Mario Carneiro (Jan 15 2019 at 15:17):

By the way there is actually a data type in mathlib for underdetermined elements, called semiquot. It is a value that lives in a set, but we don't know which element of the set it is

view this post on Zulip Joseph Corneli (Jan 15 2019 at 15:23):

Thanks for the responses -- I'm glad I didn't hesitate (too much) to post. I do still feel that there's a story to tell on the reals, and I'm only just learning the vocabulary now. Maybe I'll come back with a further iteration of the question/idea another time!

view this post on Zulip Jeremy Avigad (Jan 16 2019 at 02:59):

I am hoping to experiment soon and come up with a workable way of dealing with partial functions in the analysis library. There are multiple ways we can model the space α →. β of partial functions. We can use option β or roption β, but, as Mario points out, there are other possibilities. For example, we can use sets with at most one element. Classically, these are all isomorphic, so I don't know whether it makes much of a difference.

Nobody seems to like the name roption. Assuming we stick with that type, I have a proposal: rename roption β to partial β. Think of an element of this type as a "partial value," that is, a value that may or may not really exist. In that case, a partial function f : α →. β from α to β is, by definition, a function from α to partial β.

Cute, isn't it?

view this post on Zulip Johan Commelin (Jan 16 2019 at 06:53):

I think I like that name! :thumbs_up:


Last updated: May 08 2021 at 22:13 UTC