does "standard" theory assume |- -. +oo e. CC ?

[Glauco]

In order to prove a counterexample, I recently wrote a couple of simple theorems, proving that plus infinity and minus infinity are not complex numbers.

Before submitting the PR, a script warned me that I was using ~ df-pnf and ~ df-mnf , for which new use is discouraged.

I understand that the theory requires that plus infinity is not a real number, and df-pnf is built in such a way to ensure it ( ~ pnfnre ).

But the comment says:

" We use ` ~P U. CC ` to make it independent of the
construction of ` CC ` , and Cantor's Theorem will show that it is
different from any member of ` CC ` and therefore ` RR ` . "

And in fact, the proof of ~ pnfnre proves (step 4) that plus infinity is not a complex number. But it looks like we don't have such assertion as a standalone theorem (on purpose, I presume)


In conclusion, which of the following three statements holds?

1. the "standard" theory works perfectly fine without assuming plus infinity not being a complex number. Thus, |- -. +oo e. CC should NOT be a theorem in set.mm

2. the "standard" theory assumes that plus infinity is not a complex number and +oo has to be defined so that |- -. +oo e. CC can be "directly" proven from the definition(if this is the case, the discouraged clause should be relaxed and allow for a "direct" proof of |- -. +oo e. CC )

3. the "standard" theory assumes that plus infinity is not a complex number, but it does not depend on a particular definition of +oo, it can be proven from the standard axiomatization of the extended reals and complex numbers (if this is the case, can anybody reference a textbook proof?)

Thanks
Glauco

p.s.
the comment in ~ df-mnf seems to confirm statement 1. , I guess

[Jim Kingdon]

On 1/5/22 11:54 AM, Glauco wrote:

1. the "standard" theory works perfectly fine without assuming plus infinity not being a complex number. Thus, |- -. +oo e. CC should NOT be a theorem in set.m

As far as I could tell from a quick glance, everything would work if +oo is defined to be _i and -oo is defined to be -u _i .

At least that seems like it from the "requiring only that +∞ be a set not in ℝ" language in http://us.metamath.org/mpeuni/df-pnf.html and, backing it up, that df-pnf is only used in http://us.metamath.org/mpeuni/pnfnre.html and http://us.metamath.org/mpeuni/mnfnre.html (and a third one trivially satisfied by anything used to define RR* the way we do) and that other usages go via pnfnre .

[Glauco]

It's not clear to me why Norman used

|- +oo = ~P U. CC

in place of the more straightforward

~P U. RR

Below is a shorter proof of  pnfnre (it uses a subset of the labels, then no more axioms)

h50::pnfnre3.1        |- A = ~P U. RR
51:50:eleq1i         |- ( A e. RR <-> ~P U. RR e. RR )
52::pwuninel         |- -. ~P U. RR e. RR
53:52,51:mtbir      |- -. A e. RR
qed:53:nelir       |- A e/ RR

[Alexander van der Vekens]

Maybe Wikipedia (https://en.wikipedia.org/wiki/Infinity#Calculus) gives some hints:

* In real analysis, the symbol , called "infinity", is used to denote an unbounded limit. The notation x --> +oo means that x increases without bound, and x --> -oo means that x decreases without bound.

* In complex analysis the symbol oo, called "infinity", denotes an unsigned infinite limit. x --> oo means that the magnitude |x| of x grows beyond any assigned value.

Especially in the real case, we have the definition of superior limit  limsup which can take the values -oo and +oo, see ~ limsupcl . As far as I know, there is nothing in set.mm corresponding to the complex case.

[Alexander van der Vekens]

Maybe the current definition might leave open the possibility to use it for the complex case as mentioned in the Wikipedia article in the future...

[Benoit]

It's better to have $\pm\infty \notin \CC$ ("plus/minus infinity not in CC"), even though \pm\infty are used in a real context, so generally not together with complex numbers, so $\pm\infty \notin \RR$ would probably suffice.  This avoids more potential clashes.  We can "detach" from the proof of $+\infty \notin \RR$ the intermediate step $+\infty \notin \CC$ although it would probably not be used much, for the above reason.

Note that \pm\infinity on the one hand, and \infinity on the other hand, are the points added in the two standard compactifications of \RR, where \lim_{x \to a} can be interpreted as a limit in a topological space in the same way regardless of a being finite or infinite.  Note that in set.mm, where we like genuine inclusions, \infty should be "the same" point in the one-point (or "Alexandroff") compactification of \C, yielding the real and complex projective lines (complex projective line = Riemann sphere).  I developped in my mathbox a proposal where all these spaces fit well together, with genuine inclusions: see the section in my mathbox titled "Extended real and complex numbers, real and complex projectives lines".  (I just noticed the typo "projectives", which I'll fix soon.)

Benoît

[Thierry Arnoux]

There are other definitions of infinity on the complex plane: Benoît has for example defined the circle at infinity, with an infinite number of points at infinity (see ~ bj-inftyexpidisj), and the (single) point at infinity of the complex projective line (~ df-bj-infty). These might be used as more general versions of infinity, and we could then identify the current `+oo` and `-oo` with the corresponding points at infinity in direction 0 and π.

Glauco, can you give the actual counter example you tried to prove in the first place?
Isn't it possible to prove it within RR, using `abs`, without any need to consider `CC`?

[Benoit]

On Thursday, January 6, 2022 at 4:54:19 AM UTC+1 Thierry Arnoux wrote:

There are other definitions of infinity on the complex plane: Benoît has for example defined the circle at infinity, with an infinite number of points at infinity (see ~ bj-inftyexpidisj), and the (single) point at infinity of the complex projective line (~ df-bj-infty). These might be used as more general versions of infinity, and we could then identify the current `+oo` and `-oo` with the corresponding points at infinity in direction 0 and π.

Thanks for mentioning it.  It is already in set.mm as:

df-bj-pinfty $a |- pinfty = ( inftyexpi ` 0 ) $.

df-bj-minfty $a |- minfty = ( inftyexpi ` _pi ) $.

Benoît

[Glauco]

Hi  Thierry  ,

this is the counter example

    climlimsupcex.1 $e    |- -. M e. ZZ $.
    climlimsupcex.2 $e   |- Z = ( ZZ>= ` M ) $.
    climlimsupcex.3 $e |- F = (/) $.
    $( Counterexample for ~ climlimsup , showing that the first hypothesis is
       needed, if the empty set is a complex number (see ~ 0ncn and its
       comment) $)
    climlimsupcex $p |- ( (/) e. CC -> ( F : Z --> RR /\ F e. dom ~~> /\ -. F ~~> ( limsup ` F ) ) )

As you can see, there's already a "weird" precondition (/) e. CC  , but if you read the comment for ~ 0ncn you'll immediately see why it's there

~ climlimsup is not  published yet

    $d F k m x $. $d M k m x $. $d Z k m x $. $d k m ph x $.
    climlimsup.1 $e     |- ( ph -> M e. ZZ ) $.
    climlimsup.2 $e   |- Z = ( ZZ>= ` M ) $.
    climlimsup.3 $e    |- ( ph -> F : Z --> RR ) $.
    $( A sequence of real numbers converges if and only if it converges to its
       superior limit. The first hypothesis is needed (see ~ climlimsupcex for
       a counterexample) $)
    climlimsup $p  |- ( ph -> ( F e. dom ~~> <-> F ~~> ( limsup ` F ) ) ) $=

Anyway, for the time being, I'm going to change the counterexample in 

|- ( ( (/) e. CC /\ -. -oo e. CC ) -> ( F : Z --> RR /\ F e. dom ~~> /\ -. F ~~> ( limsup ` F ) ) ) 

I believe it does the job.

Thanks everyone for the precious help, as always.

Glauco

[Benoit]

Since (/) e. CC is false in set.mm (in real life, it should not even be false, but nonsensical), you can prove ( (/) e. CC -> anything ) so climlimsupcex does not look very useful.  Maybe there is something special in the proof, in which case that thing could be extracted to state precisely what you mean.

If a meaningful statement contains the construction ( ZZ>= ` M ) , then there is a good chance that M e. ZZ is needed.  In an ideal world, the mere writing of ( ZZ>= ` M ) should require M e. ZZ (with the current definition of ZZ>=; one could imagine a definition making sense for any argument in the extended reals).

Benoît

[Thierry Arnoux]

Thanks Glauco,

Ok, I see that your new formulation would be provable, since you have already proven ` ( limsup ` (/) ) = -oo ` in ~ limsup0.

I suppose you're just being curious about out-of-domain behavior here, and whether or not you are able to prove this counter example shall not have any impact on the broader picture, like measure theory or integration.

Did you see ~ lmdvglim ? It states that if a monotonic sequence does not converge in the real numbers in the sense of ~~> , then it converges to +oo in the topology of the extended numbers.

Maybe it could be related with what you're interested in.

Also, in his Mathbox, and commented out, Mario has a sketch of definition of an Alexandroff extension, using `~P U. X` (~ alextop; see also ~ dfac14lem and ~ kelac2lem). I think those would be interesting starting points to define one-point compactifications, and apply them to the complex plane.

BR,
_
Thierry