A better notation for limit

Stream: new members

[Arshak Parsa]

Is there a better notation for the limit in mathlib ?
like lim x → -∞ , (∫ (t : ℝ) in Iic x, f t) = 0 instead of Tendsto (fun x ↦ ∫ (t : ℝ) in Iic x, f t) atBot (𝓝 0)

[Asei Inoue]

I have a same question!

[Asei Inoue]

why arrow-like notation for the limit does not exist?

[Jireh Loreaux]

I think because no one has proposed a notation on which there is consensus that it is better than the status quo.

[Violeta Hernández]

I don't see why arrow notation couldn't be used for the more common patterns. For instance, lim x → a could consider punctured neighborhoods at a, lim x → a⁺ would be punctured right neighborhoods, etc.

[Violeta Hernández]

Admittedly, since a lot of this is specific to ℝ or ℂ, the notation might just cause more confusion down the line, since you'd still need to use the existing notation most of the time

[Arshak Parsa]

Actually, I want to introduce lean to other statisticians, but they are not used to this "Tendsto notation." Since I'm writing an article for this, I don't want to write a new notation that doesn't exist in mathlib.

[Johan Commelin]

Would something like this work?

lim x in F, f(x) tendsto G

as notation for Tendsto f F G

[Violeta Hernández]

I like that a lot

[Vincent Beffara]

Perhaps not tendsto as a keyword here, because we keep telling undergrad to write either "f tends to l" or "lim f = l" but never "lim f tends to l" so it feels wrong. But certainly lim x in F, f x whatever G would fit very well with the notation fon integrals and such!

[Arshak Parsa]

@Johan Commelin
Does this notation exist in mathlib?

[Yaël Dillies]

No, there is currently no such notation in mathlib

[Asei Inoue]

I think arrow like notation is better!

for example,

lim x in F, f(x) →ₜ G

[Etienne Marion]

I think this is as redundant as tendsto. Either the function tends to something, either the limit is equal to something.

[Vincent Beffara]

Something like f →ₜ[F] G makes sense, but it is probably too close to Tendsto to be useful.

Come to think if it, another option closer to informal use would be to have lim x in F, f x behave like docs#tsum (and then Tendsto would correspond to HasSum).

I have a Pavlovian response to "the limit tends to" but it might be PTSD from the classes préparatoires :sweat_smile:

[Etienne Marion]

Vincent Beffara said:

Something like f →ₜ[F] G makes sense, but it is probably too close to Tendsto to be useful.

I think this is a good notation, though it might be interesting to specialize it for neighbourhoods and atTop/atBot. But this would only be here for readability.

Vincent Beffara said:

Come to think if it, another option closer to informal use would be to have lim x in F, f x behave like docs#tsum (and then Tendsto would correspond to HasSum).

I agree this would be natural, it is also the way derivatives are handled. But I don't know if it's worth adding it.

Vincent Beffara said:

I have a Pavlovian response to "the limit tends to" but it might be PTSD from the classes préparatoires :sweat_smile:

I would say that strictly speaking "the limit tends to" is nonsense but maybe I have a PTSD too.

[Johan Commelin]

One benefit of having a component like x in F in the notation is that it makes it possible to also have f x as simply the body of a lambda expression.

[Vincent Beffara]

Yes, lim x in F, f x is great! But lim x in F, f x \to l does not typecheck.

[Etienne Marion]

Maybe (f x) →ₜ[x in F] G? This is certainly close to what I would write on paper

[Vincent Beffara]

Etienne Marion said:

Maybe (f x) →ₜ[x in F] G? This is certainly close to what I would write on paper

It would, but can you capture x after using it?

[Etienne Marion]

I don’t know enough about notations in Lean

[Vincent Beffara]

Something like HasLimit f x0 l to mean Tendsto f (𝓝[≠] x0) (𝓝 l) might also make sense in some cases as a way to postpone the introduction of filters

[Eric Wieser]

Vincent Beffara said:

It would, but can you capture x after using it?

I'm pretty sure you can, but it would be inconsistent with other binder notations in mathlib (such as integrals)

[Yury G. Kudryashov]

Etienne Marion said:

Vincent Beffara said:

Come to think if it, another option closer to informal use would be to have lim x in F, f x behave like docs#tsum (and then Tendsto would correspond to HasSum).

I agree this would be natural, it is also the way derivatives are handled. But I don't know if it's worth adding it.

See docs#limUnder

[Yury G. Kudryashov]

The main issue with notation is that there are so many filters that can reasonably appear as F or G in Tendsto f F G.