notation for limit

Stream: mathlib4

[Kenny Lau]

import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Order.Filter.Defs

namespace Filter

scoped syntax "lim[" term:max " → " term:max "]" term:51 "=" term:max : term

macro_rules
| `(lim[$x → $filter] $fx = $limit) =>
  `(Tendsto (fun $x ↦ $fx) $filter (nhds $limit))

scoped syntax "lim[" term:max " → " "-∞" "]" term:51 "=" term:max : term

macro_rules
| `(lim[$x → -∞] $fx = $limit) =>
  `(lim[$x → .atBot] $fx = $limit)

open Real

example : lim[x → -∞] exp x = 0 :=
  Real.tendsto_exp_atBot

end Filter

[Kenny Lau]

do we want be able to write lim, which is a more familiar notation for Filter.Tendsto?

[Kenny Lau]

let me also note that there are 1835 matches for Filter.Tendsto _ _ (nhds _)

[Kenny Lau]

and also let me note that there is precedent for little-o notation

[Weiyi Wang]

a friction from this might be that the = symbol is used for something that's not an equation, and one gets surprised when trying to rewrite with it

[Kenny Lau]

we could make grw work with this :melt:

[Kenny Lau]

we could i guess add a subscript like =ₗ to serve as reminder that this isn't Eq

[Kenny Lau]

let me also cite the widely used ModEq notation which also looks like equality

[Etienne Marion]

Related: #new members > A better notation for limit

[Kenny Lau]

@Yury G. Kudryashov I don't want to respond in new members, so i'll respond here; I propose that we only enable this notation for the filters that are nhds, atTop, atBot, and the [<] and [>] filters

[Anatole Dedecker]

I think I have another PTSD than the ones mentioned in the new members thread: I don't understand why one would prefer $\lim_{x\to a} f(x) = l$ over $f(x) \xrightarrow[x\to a]{} l$. But I may have been doing Lean for too long...

[Kenny Lau]

it's solely because that's what the maths community has decided

[Kenny Lau]

also having it look like a term makes it easier to write lim f+g = lim f + lim g

[Anatole Dedecker]

One thing I would really like to have would be something calc-like which would allow reasoning of the form $f(x) = \dots = g(x) \xrightarrow[x\to a]{} l = \dots = l'$

[Anatole Dedecker]

Maybe even with eventual equalities mixed in

[Kenny Lau]

I think grw is supposd to do that?

[Kenny Lau]

anyway this is off topic

[Anatole Dedecker]

Yes sorry

[Kenny Lau]

so anyway @Anatole Dedecker would you like to see this notation in mathlib

[Yury G. Kudryashov]

We had a similar notation for limits of sequences, then removed it.

[Kenny Lau]

why?

[Yury G. Kudryashov]

Let me find the discussion.

[Sébastien Gouëzel]

Having lim[x → -∞] exp x = 0 where the equal sign is not the usual one and lim[x → -∞] exp x isn't a thing by itself just looks like a crazy source of confusion to me.

[Kenny Lau]

I proposed changing the equal sign to =ₗ, does that solve this problem?

[Anatole Dedecker]

One thing I worry about is that any attempt to hide the filter in the notation is just pushing back the problem to "all the lemmas mention filters and you have to know their names".

[Kenny Lau]

that is indeed a problem...

[Kenny Lau]

but we can make this information show up on hover?

[Kenny Lau]

i think without the notation you still have the same problem, "we only have filters so you have to state limit in terms of filters"

[Anatole Dedecker]

Sébastien Gouëzel said:

Having lim[x → -∞] exp x = 0 where the equal sign is not the usual one and lim[x → -∞] exp x isn't a thing by itself just looks like a crazy source of confusion to me.

I agree. If people really want such a notation it should be notation for docs#limUnder.

[Anatole Dedecker]

Kenny Lau said:

i think without the notation you still have the same problem, "we only have filters so you have to state limit in terms of filters"

I'm not claiming your proposal creates the problem, I'm claiming it doesn't really solve it.

[Yury G. Kudryashov]

Here is the PR that removed the notation we had: https://github.com/leanprover-community/mathlib3/pull/15696

[Kenny Lau]

what was the reason?

[Kenny Lau]

Anatole Dedecker said:

I agree.

Would you agree if I changed = to =ₗ?

[Yury G. Kudryashov]

We may decide to rename lim to something, then rename limUnder to lim and add API about it as we have API about HasDerivAt and deriv.

[Yury G. Kudryashov]

The old notation was x \longrightarrow a and only worked for sequences.

[Yury G. Kudryashov]

The current approach is to make people read Math in Lean or something like that.

[Anatole Dedecker]

Yury G. Kudryashov said:

We may decide to rename lim to something, then rename limUnder to lim and add API about it as we have API about HasDerivAt and deriv.

This is I think the most sensible approach. I don't quite see the interest myself because I essentially never write "the limit equals" even on paper, but that's a matter of taste.
One problem: this means adding a predicate of the form "this has some limit" as a condition for limUnder lemmas.

[Kenny Lau]

given that we currently don't have API for limUnder i would think that having notation for Filter.Tendsto might be a better short-term approach

[Kenny Lau]

(and more constructive??)

[Kenny Lau]

Yury G. Kudryashov said:

The current approach is to make people read Math in Lean or something like that.

i'm not sure what you meant with this sentence

[Kenny Lau]

Anatole Dedecker said:

This is I think the most sensible approach.

I feel like this as well only pushes the problem back, because now when you're proving any limit you need to

1. change the goal to be in the form of Filter.Tendsto
2. and then use the standard lemmas for chaining limits (we're still missing the fun_prop extension that can automatically prove limits)

[Kenny Lau]

and I would think that when you're performing step 2 it might be better to see the limit notation

[Etienne Marion]

Kenny Lau said:

Yury G. Kudryashov said:

The current approach is to make people read Math in Lean or something like that.

i'm not sure what you meant with this sentence

I think he means that we point people to the book Mathematics in Lean which is a great resource to learn about filters both in general and in mathlib.

[Kenny Lau]

i mean, seeing that we'll need both anyway, what if we just have notation for both?

[Kenny Lau]

ah, right i forgot about that book, i think I usually see it abbreviated as #mil

[Kenny Lau]

Anatole Dedecker said:

"all the lemmas mention filters and you have to know their names"

well... we could also change the names after we introduce this notation...

[Alex Meiburg]

That seems like an even larger trap. Naming conventions should be based on the names of the objects, generally, and the theorems should be in appropriate generality; having theorems with strings lim_eq in the name when they're about a filter tending to a value ... seems much worse

[Kenny Lau]

how do you propose to solve this problem?

[Sébastien Gouëzel]

I don't see a problem here. Writing lim f = a is bad mathematical practice, and should be discouraged, also in paper math.

[Yury G. Kudryashov]

The current solution is to use Filter.Tendsto and let people read #mil to see how to express lim_{x\to _} f(x) = _ in Lean.

[Yury G. Kudryashov]

Sébastien Gouëzel said:

I don't see a problem here. Writing lim f = a is bad mathematical practice, and should be discouraged, also in paper math.

OTOH, we support this kind of notation for derivatives, infinite sums, and intergrals.

[Kenny Lau]

we currently have notation for all kinds of nhds-related filters already, surely it isn't a stretch to extend that notation to Filter.Tendsto so that we don't have to write "Tendsto .. nhds" all of the time

[Kenny Lau]

again we don't have to use the equal sign!

[Kenny Lau]

what if we write exp (-x) →[x → ∞] 0 or exp (-x) ⟶[x → ∞] 0?

[Sébastien Gouëzel]

We have this kind of notation for derivatives, infinite sums, and integrals, because these are things which are used all the time in computations. This is not the case for limits as far as my practice tells.

[Sébastien Gouëzel]

(If you want to use it for limits, we already have this concept, it's called limUnder. But in practice it's very rarely used, because it's not useful)

[Kenny Lau]

is it possible that it's not widely used right now because we're lacking some API?

[Sébastien Gouëzel]

If people had needed it, they would probably have added the API long ago.

[Kenny Lau]

i mean, how would you prove that x ^ x ⟶[x → 0+] 1? I would imagine you would want to use the APIs

[Sébastien Gouëzel]

Note that I would be perfectly fine with a notation like exp (-x) →[x → ∞] 0. But that's orthogonal to using more limUnder.

[Kenny Lau]

well with all of these classical functions you end up just deferring the proof to a later step, you still have to prove sooner or later that the limit actually exists

[Kenny Lau]

Sébastien Gouëzel said:

Note that I would be perfectly fine with a notation like exp (-x) →[x → ∞] 0. But that's orthogonal to using more limUnder.

that's fine, we can discuss using limUnder more in a different thread

[Kenny Lau]

Do other people here agree with exp (-x) ⟶[x → ∞] 0?

[Adam Topaz]

Another approach is to define a class Filter.HasLimit : Prop as an existential, then add Lim F as a choice of witness and whatever notation for special filters. The equality above would then be a legitimate equality. I think we already do something like this (without notation) for ultrafilters?

[Kenny Lau]

that's even worse, now you can't rewrite anything, I think we have this practice of separating proofs and definitions (and make all functions total) for this exact reason

[Sébastien Gouëzel]

That's essentially what limUnderis: if there is a limit, pick one, otherwise use a junk value. In practice, this has not proved useful.

[Adam Topaz]

Ok fair enough

[Kenny Lau]

like, consider the ⁻¹ for fields vs. the Invertible typeclass stuff

[Kenny Lau]

we love total functions so much we ended up having Units.mk0 in the library

[Kenny Lau]

Kenny Lau said:

Do other people here agree with exp (-x) ⟶[x → ∞] 0?

@Yury G. Kudryashov are you ok with this notation? (since Sebastien and Anatole seem to be ok with it)

[Kenny Lau]

for the orthogonal discussion I think the classical functions such as sum are more usable because its junk value 0 makes sense for this additive context; for limit (e.g. my example x^x -> 1 above) it wouldn't work because exp sends junk value 0 to the non-junk value 1, so we can't write lim (exp f) = exp (lim f) sadly

[Weiyi Wang]

Another question: the undergrad definition of "lim_{x->a} f(x) = b" corresponds to 𝓝[≠] a and 𝓝 b if I understand correctly. If we introduce notation like f(x) ->[x->a] b to mean the undergrad lim, are we ok with having two kinds of filter under the hood?

[Kenny Lau]

@Weiyi Wang do we even want that in the first place? the normal one has 117 matches and the punctured one has 76 matches so to my surprise they're both used, but I would imagine that we would want to write x → ≠a for the punctured one

[Weiyi Wang]

I don't know whether we want it or not. If the goal is to introduce notation that more people are familiar with, then it should follow the conventional definition of that notation as well. If the goal is to just make the statement prettier, then this isn't an issue

[Kenny Lau]

@Weiyi Wang while that is indeed a valid concern, i think there are two counterpoints that outweigh it,

1. I want other types of limits as well, such as inf, -inf, a+, a-, and for the sake of consistency i would want the source and target filters to have the same meaning
2. it shouldn't be that hard to get used to writing an extra ≠ to mean punctured
3. if we default to the punctured, we would have no way to write the normal nhds

[Sébastien Gouëzel]

Weiyi Wang said:

Another question: the undergrad definition of "lim_{x->a} f(x) = b" corresponds to 𝓝[≠] a and 𝓝 b if I understand correctly.

This depends on where you've studied. In France, it's 𝓝 a and 𝓝 b.

[Snir Broshi]

Sébastien Gouëzel said:

Weiyi Wang said:

Another question: the undergrad definition of "lim_{x->a} f(x) = b" corresponds to 𝓝[≠] a and 𝓝 b if I understand correctly.

This depends on where you've studied. In France, it's 𝓝 a and 𝓝 b.

So $\lim_{x \to 0} \frac{sin(x)}{x}$ is undefined in France undergrad? Or is it handled like an exception?

[Etienne Marion]

You write $\lim_{\substack{x \to 0 \\ x \ne 0}} \frac{\sin(x)}{x}$ (or leave it to the reader to interpret correctly, because it is quite obvious actually)

[Damiano Testa]

When I learned limits, many years ago in Italy, the convention was also that for limits of a real function it was (usually implicit) that the variable was required to be different from its limiting value.

[Snir Broshi]

Etienne Marion said:

You write $\lim_{\substack{x \to 0 \\ x \ne 0}} \frac{sin(x)}{x}$ (or leave it to the reader to interpret correctly, because it is quite obvious actually)

Well then the conventions differ only when the function is defined but discontinuous.
I think such functions aren't that common except when defined a function by cases: if x = 0 then 42 else x

[Weiyi Wang]

It matters more in mathlib because sin x / x is defined everywhere and discontinuous

[Floris van Doorn]

Weiyi Wang said:

Another question: the undergrad definition of "lim_{x->a} f(x) = b" corresponds to 𝓝[≠] a and 𝓝 b if I understand correctly.

In the Netherlands we used the same convention as France's (but I can very well imagine it's lecturer-dependent).

Is the one you mentioned the US convention? It must be tough for the chain rule to fail if you use that convention:
"if lim_{x->a} f(x) = b and lim_{x->b} g(x) = c then lim_{x->a} g(f(x)) = c"

[Weiyi Wang]

I learned in Chinese and it was the convention there, and indeed the chain rule was stated in a very complicated way because of this

[Weiyi Wang]

English wikipedia seems to be following the punctured filter convention

[Kenny Lau]

I mean, you want (f y - f x) / (y - x) to tend to f’(x)

[Etienne Marion]

But in paper maths the function is not defined at x so it is obvious that you only consider y ≠ x. And if it might be ambiguous or confusing for the reader (for instance if it is a student who is not familiar with the notation) then you can add the y ≠ x below the y -> x.

[Kenny Lau]

Etienne Marion said:

it is obvious that you only consider y ≠ x.

but this is illegal

[Yury G. Kudryashov]

In Russia, it's the punctured nhds by default, so the chain rule requires the outer function to be continuous at a point.

[Jireh Loreaux]

Kenny Lau said:

Do other people here agree with exp (-x) ⟶[x → ∞] 0?

If we were coming up with some notation for Filter.Tendsto, as we have considered numerous times before, I think we should consider the specification before introducing the notation.

I think the key question is this: should it support Tendsto f l l' for arbitrary filters l and l'? If not, why not, and which special filters should it support?

To explain why this is such a thorny question, consider the following. On the one hand, it would be quite easy to suggest that it should support 𝓝 a, atTop, atBot and 𝓝[≠] a, but also 𝓝[<] a and 𝓝[>] a are quite common. Note that on paper, we only really have notation for the latter three as the filter on the domain; that is, we have no way to write Tendsto arctan atTop (𝓝[<] (π / 2)). Should the notation support these in the codomain? There's others that come up semi-frequently, such as taking the limit as ‖z‖ → ∞, which corresponds to the cobounded filter. There's also the issue that the notation x → ∞ for atTop isn't so great unless the function has ℝ or ℕ as it's domain (e.g., it's bad for atTop : Filter (Finset ℕ)).

Given the previous paragraph, in my mind it doesn't make too much sense to only support specific filters, because you either end up supporting very few, and the notation quickly becomes not usable, or you end up supporting many, and the notation becomes very cluttered or doesn't generalize well to functions with other domains / codomains. But I've never been able to come up with different notation I liked well enough that worked for arbitrary filters that was shorter than Tendsto f l l'.

In my mind, the whole thing is a non-issue. When learning formalization, one must learn that filters are really the answer, even for paper mathematics, and at that point, why not stick to Tendsto?

[Jireh Loreaux]

Additionally, keeping the 𝓝 around really helps you to remember that you need your space to be Hausdorff (so that you can use docs#tendsto_nhds_unique to show that a = b when they are each limits of the same function).

[Kenny Lau]

@Jireh Loreaux
image.png

This is the specification, and I think it covers enough cases, note that as you probably know we also have syntax for special filters which has worked fine

[Jireh Loreaux]

The fact that we have special syntax for those filters is exactly one of the reasons I don't think we need this.

[Jireh Loreaux]

e.g., Tendsto arctan atTop (𝓝[<] (π / 2)) is pretty readable, no?

[Kenny Lau]

surely arctan x ⟶[x → ∞][<] π / 2 is even more readable

[Etienne Marion]

Jireh Loreaux said:

In my mind, the whole thing is a non-issue. When learning formalization, one must learn that filters are really the answer, even for paper mathematics, and at that point, why not stick to Tendsto?

That's also my opinion.

[Kenny Lau]

Jireh Loreaux said:

When learning formalization, one must learn that filters are really the answer, even for paper mathematics

I think it helps to have more familiar notation, if we want to attract new undergrads and make the entry bar lower

[Yury G. Kudryashov]

Kenny Lau said:

surely arctan x ⟶[x → ∞][<] π / 2 is even more readable

Unless you recognize this notation, you can't be sure that < applies to pi / 2.

[Kenny Lau]

that's a fair point, maybe we can have another notation for codomain

[Kenny Lau]

how would you write it in paper maths? $(\pi/2)^-$?

[Jireh Loreaux]

This was one of my points: we don't really allow that on paper.

[Yury G. Kudryashov]

I think that notation won't help. You need to learn about filters to deal with topology and analysis in Mathlib. Once you do, Tendsto is more readable than this notation.

[Etienne Marion]

Kenny Lau said:

Jireh Loreaux said:

When learning formalization, one must learn that filters are really the answer, even for paper mathematics

I think it helps to have more familiar notation, if we want to attract new undergrads and make the entry bar lower

Is notation for limits really the thing that prevents undergrads from learning formalization? I am really asking the question, I would be very surprised if the answer is yes. I started lean as an undergrad and compared to other things learning to use filters and Tendsto was a cake walk (and very interesting mathematically as well).

[Jireh Loreaux]

Kenny Lau said:

surely arctan x ⟶[x → ∞][<] π / 2 is even more readable

No, because it's not clear x → ∞ is even a filter.

[Kenny Lau]

I meant readable from the point of view of someone who doesn't know filters

[Lua Viana Reis]

Jireh Loreaux said:

we have no way to write Tendsto arctan atTop (𝓝[<] (π / 2))

perhaps not in an undergraduate course setting, but I often see this written as $\lim_{x \to \infty} \arctan(x) \nearrow \frac \pi 2$

[Kenny Lau]

yeah i was indeed thinking about arrows

[Jireh Loreaux]

Kenny Lau said:

I meant readable from the point of view of someone who doesn't know filters

but then you're just obfuscating what's really going on, making it more difficult when they try to use it or prove things about it.

[Kenny Lau]

↗ could work for domain too

[Etienne Marion]

A limit does not tend to something, using both lim and an arrow is nonsense.

[Kenny Lau]

right, my notation doesn't say lim at all

[Lua Viana Reis]

Kenny Lau said:

yeah i was indeed thinking about arrows

that said, I did not say I like it :p

[Etienne Marion]

Kenny Lau said:

I meant readable from the point of view of someone who doesn't know filters

But if they don't know filters they will have a hard time doing formalization which involves limits anyway.

[Kenny Lau]

i mean if you're computing a limit like lim(f+g) = lim f + lim g you don't need filter for that

[Kenny Lau]

also, at least the statements look nicer

[Lua Viana Reis]

What about some sort of As x → atTop, arctan x → 𝓝[<] (π / 2)? I don't want to advocate for more notation, but I like that it seems more readable and also binds the x on the left, like most notations.

[Jireh Loreaux]

This is the kind of thing I've come up with in the past (it supports arbitrary filters), but I never decided it was any better than a bare Tendsto.

[Lua Viana Reis]

And if you really want, you could write the version As x → ∞, arctan x ↗ π / 2, but I think this obfuscates things.

[Weiyi Wang]

Maybe we just need a notation for atTop? like →∞?

[Snir Broshi]

IMO readability of the docs should be a goal, I think docs#tendsto_fib_succ_div_fib_atTop looks pretty poor in the docs compared to $\lim_{n \to \infty} \frac{\text{fib }(n+1)}{\text{fib }n} = \varphi$.
Though I'm not sure why the docs don't render 𝓝 and φ, which would also help for readability.

Also I prefer a notation that'll work with calc (as Anatole mentioned) over readability.
Maybe something like tsum but for limits, perhaps called tlim?

[Kenny Lau]

Weiyi Wang said:

Maybe we just need a notation for atTop? like →∞?

might I suggest 𝓝 ∞

[Jireh Loreaux]

please no.

[Kenny Lau]

Snir Broshi said:

Though I'm not sure why the docs don't render 𝓝 and φ

docs don't use scoped notation

[Kenny Lau]

we could do ↗∞

[Jireh Loreaux]

Kenny Lau said:

might I suggest 𝓝 ∞

That would be ultra confusing in situations when ∞ is actually a term of your type (e.g., ℝ≥0∞ or OnePoint)

[Kenny Lau]

I think you use \top for ENNReal?

[Jireh Loreaux]

in the ENNReal scope ∞ is allowed, but we use top in declaration names (since it's just notation).

[Etienne Marion]

Snir Broshi said:

Also I prefer a notation that'll work with calc (as Anatole mentioned) over readability.
Maybe something like tsum but for limits, perhaps called tlim?

docs#limUnder

[Kenny Lau]

is atTop the same filter as nhds \top?

[Yury G. Kudryashov]

No, in an OrderTop, atTop = pure \top.

[Jireh Loreaux]

Kenny, you have yet to convince me that this is a problem that needs solving. I suggest you come up with a collection of examples (not from the docs because those don't render scoped notation and that's a separate issue) where the bare Tendsto is really bad and could be improved with notation.

[Kenny Lau]

@Jireh Loreaux Does Snir's example suffice?

[Jireh Loreaux]

no, in the source this is:

Tendsto (fun n ↦ (fib (n + 1) / fib n : ℝ)) atTop (𝓝 φ)

Please explain what's so terrible about that.

[Kenny Lau]

well firstly Tendsto goes at the beginning whereas in words we would say ".. tends to phi", this is the same reason why we have notations for infix so we don't say Add.add 3 4
and secondly there's the atTop thing which looks a bit disconnected from "infinity"
and then thirdly we don't really think about "neighbourhood" normally, at least not in the statement

[Snir Broshi]

Terrible is subjective, I'm not sure it can be explained

[Weiyi Wang]

I personally would vote for "bare Tendsto is not an issue". When I see the first Tendsto statement when learning, I quickly guessed what it means without reading much guide. On the other hand, I find myself often needing to consult doc for things with custom notation. Maybe because I came from programming and read bare functions more quickly

[Thomas Murrills]

(Meta: I think the bar should be "does having notation improve things", rather than "is the current state of affairs bad". :) )

[Kenny Lau]

well, which "things"? I think different people here are focusing on different things

[Thomas Murrills]

Coming to a consensus on that is what this discussion is (partially) for. :grinning_face_with_smiling_eyes:

[Jireh Loreaux]

Kenny Lau said:

well firstly Tendsto goes at the beginning whereas in words we would say ".. tends to phi", this is the same reason why we have notations for infix so we don't say Add.add 3 4

This is the best reason I've heard you give (in my opinion). However, note that your approach means that we write everything in a (sort of) eta-expanded form. I'll note that we do take this approach in other places throughout the library, notably in integration, but not everywhere. So for instance, your notation would allow to talk about the function fun x ↦ (g ∘ f) x, but not (g ∘ f). This is enough of an issue that we regularly have both versions in various places throughout the library.

and secondly there's the atTop thing which looks a bit disconnected from "infinity"

yeah, well that's because atTop is more general, so I don't feel bad about this. In any case, that sounds like you want notation for atTop, which is a separate question.

and then thirdly we don't really think about "neighbourhood" normally, at least not in the statement

I'm not sure who "we" is here, but I would argue that "we" should think about neighborhoods. It was mentioned earlier in the thread that the "lim" notation common in undergraduate courses can either be 𝓝 a or 𝓝[≠] a, and I think that not enough time is spent on this distinction.

[Thomas Murrills]

(My only point is that we should probably lower the rhetorical burden from "argue that the current state of affairs is bad" to "argue that notation is better".)

[Kenny Lau]

Jireh Loreaux said:

I'll note that we do take this approach in other places throughout the library

in many cases in fact, exists, forall, Finset.sum

[Kenny Lau]

Thomas Murrills said:

argue that notation is better

so firstly we can separate out the binder which I think is a good thing, i.e. from
fun n ↦ (fib (n + 1) / fib n : ℝ)
to
(fib (n + 1) / fib n : ℝ) ⟶[n → ..] ..
since we separate out the binder in other places as well (e.g. Finset.sum)

and then having notation for atTop is also a good thing (is "atTop" even used in paper maths?)

and then not having to write 𝓝 twice is also good (we know it's about neighbourhood already)

[Thomas Murrills]

Kenny Lau said:

so firstly we can separate out the binder which I think is a good thing

Jireh Loreaux said:

So for instance, your notation would allow to talk about the function fun x ↦ (g ∘ f) x, but not (g ∘ f). This is enough of an issue that we regularly have both versions in various places throughout the library.

To address both of these: how common is Tendsto /- (expression not starting with fun) -/ ..., actually, in practice? :eyes:

[Thomas Murrills]

Kenny Lau said:

and then having notation for atTop is also a good thing (is "atTop" even used in paper maths?)

I agree notation would be good for this! :) (Although it's technically a separate topic--surely any notation should not be limited to TendsTo!)

[Yury G. Kudryashov]

Jireh Loreaux said:

Kenny Lau said:

well firstly Tendsto goes at the beginning whereas in words we would say ".. tends to phi", this is the same reason why we have notations for infix so we don't say Add.add 3 4

This is the best reason I've heard you give (in my opinion).

We move lots of predicates that make more sense as infix to the start, e.g., HasSum, HasDerivAt etc.

[Thomas Murrills]

Kenny Lau said:

and then not having to write 𝓝 twice is also good (we know it's about neighbourhood already)

I'm not 100% sure readability goes up in this case just because redundant characters go down. I think introducing non-uniformity into ways to say things can have a cognitive cost; this cost can indeed be offset by the fact that the new version is "cleaner", or if it's used enough, or if it's obvious enough, though. Similarly, removing these characters obfuscates what's "really going on", so there's an extra layer of indirection we're demanding from the reader, and indirection introduces its own issues with comprehension and uptake...

I'm also very pro-notation, but I do think it's worth being careful about the costs. I think it's easy to end up creating a labyrinth! :grinning_face_with_smiling_eyes:

[Jireh Loreaux]

Thomas Murrills said:

To address both of these: how common is Tendsto /- (expression not starting with fun) -/ ..., actually, in practice? :eyes:

Well, I gave docs#Filter.Tendsto.comp as an example, but there are also things like docs#Real.tendsto_exp_atBot, docs#Real.tendsto_exp_atBot_nhdsGT, docs#Real.tendsto_sin_pi_div_two and plenty of others. In contrast, we also have the other form: docs#Filter.Tendsto.mul.

In all honesty, it's probably not too much of an issue as it would only potentially break a few rws, but probably not simps. It was just something I noticed.

[Thomas Murrills]

If it's just an expression issue rather than a readability issue, we could of course just eta-reduce the resulting expression during elaboration--I'm not sure if this would cause other confusing behavior, but if we go with eta-expanded notation, it could be worth trying...

[Thomas Murrills]

Tangent, but can you think of existing "eta-expanded" notation where that causes an issue? Maybe it would be worth trying to eta-reduce in those notations too? :eyes:

[Jireh Loreaux]

Thomas, I'm not sure where it is, but see the naming convention discussion for mul vs. fun_mul.

[Thomas Murrills]

This discussion?

[Jireh Loreaux]

It's not about notation specifically, but just about the difference causing some issues.

[Jireh Loreaux]

(Note also that fun x ↦ f x * g x is not exactly the eta expanded form of f * g, which would be fun x ↦ (f * g) x, so there's an extra rewrite involved)

[Thomas Murrills]

Let's call an expression like fun x ↦ f x * g x a "nontrivially" eta-expanded form of f * g; after skimming the thread, am I right in thinking that this is an issue for TendsTo regardless of any notation, and that notation might only encourage nontrivial eta-expansions, rather than actually pose a problem per se?

[Alex Meiburg]

There's also the issue that the notation x → ∞ for atTop isn't so great unless the function has ℝ or ℕ as it's domain (e.g., it's bad for atTop : Filter (Finset ℕ)).

I think x → ⊤ would be the obvious choice here, no? I think most anyone actually working with this notation will at least understand that ⊤ is a less fancy way of writing ∞. (Likewise for -∞ / bottom)

[Jireh Loreaux]

What is x? My point is that if we have notation for atTop, it should work anywhere, not just in Tendsto expressions where the variable is captured by some notation.

[Patrick Massot]

In 2018 I was guilty of introducing the stupid notation that Yury mentioned and got removed in https://github.com/leanprover-community/mathlib3/pull/15696. I was ignorant about limits at that time, and I thought it would make things easier. Then it became more and more embarrassing and confusing until it was removed. I think we shouldn’t redo a larger scale version of that mistake. Sometimes I even find it embarrassing that we have Tendsto φ F G instead of simply unobfuscate it and write the intuitive map φ F ≤ G.

[Patrick Massot]

And indeed there is no denying that anyone who wants to use limits in Mathlib need to learn at least a bit of filter theory. Using a notation to postpone that need for a couple of minutes is definitely not worth all the downsides of this.

[Patrick Massot]

The question is completely different if you teach first year students using Lean. There you either need to completely redefine limits to use more elementary definitions or indeed find a way to hide filters completely.

[Aaron Liu]

though map φ F ≤ G might be more intuitive (and it's not necessarily more intuitive to everyone!), we could also just as well write F ≤ comap φ G, so I think having Tendsto φ F G is good to standardize it

[Patrick Massot]

And the long debate about neighborhoods vs punctured neighborhoods is part of the reasons why filters are so much cleaner. There is no ambiguity and the composition theorem is clear.

[Patrick Massot]

Aaron, this is indeed one reason to have a definition, but also constantly reproving Tendsto.comp would be tiresome.

[Aaron Liu]

Patrick Massot said:

Aaron, this is indeed one reason to have a definition, but also constantly reproving Tendsto.comp would be tiresome.

what do you mean constantly? don't we only prove it once?

[Patrick Massot]

Sure, we prove it only once. And of course we could state it without the definition (just unfold the definition in the current statement), but the statement would be longer to mentally parse. Alternatively we could inline the proof since it’s so short. But it’s used so often that it would be very tiresome.