Why ^pm CC in the definition of convergence w.r.t. a topology? (same for Cauchy sequences)

[Glauco]

The definition ~ df-lm  is

|- ~~>t = ( j e. Top |-> { <. f , x >. | ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )

thus, it can only be applied to functions partially defined on ` CC `.

But the relation only depends on the behavior of the function on an upperset of integers, see ~ lmres

Unless I'm missing something here, I would prefer a definition like ~ df-clim

|- ~~> = { <. f , y >. | ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) }

where no restriction on the domain of ` f ` is imposed (please, see ~ climres and compare it to ~ lmres )

In any event, why does ` CC ` even come into play, in ~ df-lm ?


Here is a first guess for an alternative ~ df-lm   (I've not tried to work with it, thus in principle it could be wrong)

|- ~~>t = ( j e. Top |-> { <. f , x >. | ( x e. U. j /\ A. u e. j ( x e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( f ` k ) e. u ) ) } )


Glauco

p.s.
with a quick search for " ^pm CC " ,  ~ df-cau comes up; I've not worked much with it, but at first look it rises the same question

[Benoit]

The definition is a bit strange indeed, and the comment could be more precise.  It was probably designed for sequences.  It looks like (x \mapsto sin(2k \pi) ~~>t 0 with this definition.

The best thing would be to derive it from a general notion of limit of functions between two topological spaces, applied to +\infty in RR* (or in df-bj-ccbar). In the meantime, it could take the form:

|- ~~>t = ( j e. Top |-> { <. f , x >. | ( f e. ( U. j ^pm RR ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. RR ( A. x e. dom f ( y < x -> ( f ` x ) e. u ) ) } )

although I would prefer to use topological spaces (df-topsp) instead of topologies.  It would make things clearer. It would something like

(* Define the function which associates with a given topological J space the relation "f ~~>t x" meaning "the partial function f from RR to J converges to x at +oo".  This can be applied in particular to sequences with values in J. *)

|- ~~>t = ( j e. TopSp |-> { <. f , x >. | ( f e. ( ( Base ` j ) ^pm RR ) /\ x e. ( Base ` j ) /\ A. u e. ( TopOpen ` j ) ( x e. u -> E. y e. RR ( A. x e. dom f ( y < x -> ( f ` x ) e. u ) ) } )

Benoît

[Benoit]

As for df-cau, I think it is expressed in a complicated way (why use balls, for instance?). It could be:

|- Cau = ( x e. MetSp |-> { f : NN0 --> ( Base `x ) /\ A. e e. RR+ E. n e. NN0 E. A. k e. ( ZZ>= ` n ) A. l e. ( ZZ>= ` n )  ( ( f ` k ) ( Metric ` x ) ( f ` l ) ) < e ) } )

(provided there is a "Slot" for the (extended) metric of a metric space).  It might be better to define it for uniform spaces.  Maybe one could allow functions defined on ( ZZ>= ` n ) for n \in ZZ.

Benoît

[Mario Carneiro]

The current definition of df-cau has fewer quantifiers and is also shorter. The switch to using structures is also breaking; I would want to see whether it leads to a shortening in theorems since you might have a raw distance function and wrapping it in a structure might cause issues.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b1475dc5-5b9e-41ed-93d7-72f841be5b82n%40googlegroups.com.

[Benoit]

On Sunday, January 23, 2022 at 4:46:01 PM UTC+1 di....@gmail.com wrote:

The current definition of df-cau has fewer quantifiers and is also shorter.

We can prove a few theorems of the form

F e. ( Cau ` X ) <-> ....

where each of these characterizations might have an advantage in different cases.  As for which characterization serves as "the" definition, this is secondary once we have these characterizations, but I think the one I proposed was easier to understand, closer to textbook definitions, and was not using constructions such as ( y ( ball `d ) x ) (meaning: the open ball of center y and radius x for the metric d).

 

The switch to using structures is also breaking; I would want to see whether it leads to a shortening in theorems since you might have a raw distance function and wrapping it in a structure might cause issues.

It would probably make proofs longer, because of the packaging/unpackaging, as you wrote.  But it would offer a more unified framework across set.mm, it seems to me, instead of sometimes defining notions on "structured sets" (set.mm's "extensible structures"), and sometimes using the specific raw structure (here: the metric itself, or the topology itself) instead of the structured set (here: the metric space, the topological space).

Anyway, I'm not going to change it, and I think Glauco's initial question was about the domain of the function (i.e., why CC instead of NN0).

Benoît

[Mario Carneiro]

Oh, I just noticed there is another issue with your definition, which might help explain why ^pm CC is used: You are requiring that f is a function on NN0, but we want it to work for functions that are only "eventually defined" on upper integers. In particular, we don't want to single out any particular upper integer set here, it should work just as well for NN and NN0, or (ZZ>=`37). I think you could get away with ^pm ZZ for this, but it's also sometimes convenient to use functions with a predetermined domain like RR or CC.

--

You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b1f2d238-6165-4928-b627-d571c8f17346n%40googlegroups.com.

[Benoit]

On Sunday, January 23, 2022 at 8:42:15 PM UTC+1 di....@gmail.com wrote:

Oh, I just noticed there is another issue with your definition, which might help explain why ^pm CC is used: You are requiring that f is a function on NN0, but we want it to work for functions that are only "eventually defined" on upper integers. In particular, we don't want to single out any particular upper integer set here, it should work just as well for NN and NN0, or (ZZ>=`37). I think you could get away with ^pm ZZ for this, but it's also sometimes convenient to use functions with a predetermined domain like RR or CC.

Indeed, and I mentioned this in my previous message:

> (provided there is a "Slot" for the (extended) metric of a metric space).  It might be better to define it for uniform spaces.  Maybe one could allow functions defined on ( ZZ>= ` n ) for n \in ZZ.

If a function is defined on a larger domain, then it is not a sequence, hence not a Cauchy sequence.  Restricting it to NN0 may yield one.

 

Benoît

[Mario Carneiro]

Sure, but that seems a bit pedantic. It induces a sequence in the obvious way. Arguably you could have a different notion of convergence for functions with more general domain, along the lines of df-rlim, but the minimalistic assumptions in df-cau are enough to prove most of the usual theorems and there is no need to be picky.

--

You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ec3cec80-8dad-47c9-a757-ed2681a176fdn%40googlegroups.com.

[Benoit]

As long as one is willing to accept that the (rescaled) sine function ( x e. CC |-> (sin ` ( _pi x. x ) ) ) is both an unbounded holomorphic function and a Cauchy sequence, all is fine.