Should iset.mm have a notation for "convergence with a modulus of convergence"?

[jkingdon]

Right now, iset.mm defines the ~~> notation exactly as in set.mm : compare https://us.metamath.org/ileuni/df-clim.html with https://us.metamath.org/mpeuni/df-clim.html . iset.mm then says that this kind of convergence holds if there is a modulus of convergence, for example in theorems such as https://us.metamath.org/ileuni/climcvg1n.html . But using this definition we don't have the ability to go back from ~~> to a modulus of convergence (apparently this would be possible with countable choice, but we don't want to assume that globally and we shouldn't need it if we arrange these theorems a bit differently).

Our choices seem to be:

1. document the current situation and continue down the path of proving various theorems which enable us to show convergence, with hypotheses for a modulus of convergence where needed. For example cvgcmp2n as shown at Show that real number trichotomy implies LPO #3423 (comment)
2. redefine ~~> to a definition which means convergence with a modulus of convergence
3. introduce two notations, ~~> as defined in set.mm and a new notation for convergence with a modulus of convergence
4. No new notation or changes to definitions but do dabble a bit in theorems like ( A e. CC /\ F : ZZ --> CC /\ E. g e. ( ZZ ^m RR+ ) A. x e. RR+ A. k e. ( ZZ>= ` ( g ` x ) ) ( ( abs ` ( ( F ` k ) - A ) ) < x ) ) ) ) -> F ~~> A ) (where the antecedent is intended to spell out convergence with a modulus of convergence, and probably could be expressed slightly differently). Given the length of that antecedent I suppose there would only be so much dabbling you'd do until you made a notation.

Options 1 and 3 would seem to be better from the point of view of keeping set.mm and iset.mm similar where possible

Options 2 and 3 would appear to make it easier to show convergence in contexts like #3423 . That particular one doesn't seem super hard with option 1 but I don't know if the convergence theorems would proliferate or become cumbersome under option 1.

Even if we want option 2 as the eventual end state we might need option 3 as an intermediate stage, depending on how many proofs would need to change.

For more background and further thoughts, see #3423 (comment)

This also might call for a certain amount of literature review especially on matters of terminology or on what definitions seem to be most common in various constructive works.

[tirix]

It looks like a new definition would be handy in this case.

[david-a-wheeler]

I agree with @tirix - the "new definition" sounds like a plausible starting point to me. But I'd love to hear from those with far more experience than me.

[jkingdon]

I agree with @tirix - the "new definition" sounds like a plausible starting point to me. But I'd love to hear from those with far more experience than me.

Unless I'm missing something (which is possible - finding and correctly understanding references in constructive analysis is not always easy), the underlying mathematics are:

1. convergence with a modulus of convergence does have the potential to simplify some proofs - in particular because the analogue of https://us.metamath.org/mpeuni/cvgcmp.html and perhaps similar theorems would hold.
2. we don't have any proofs that a sequence is convergent which would not be capable of showing a modulus of convergence. For example, in https://us.metamath.org/ileuni/climcvg1n.html the modulus is fairly directly available. The proof of https://us.metamath.org/ileuni/geolim.html goes through a different path which leads to https://us.metamath.org/ileuni/divcnv.html but there too the modulus could be provided.

So why might I appear to be hesitating? Well basically it is just a question of it seeming like a fairly big project to develop this as far as, say, showing that geolim or https://us.metamath.org/ileuni/efcllem.html satisfies the new definition. That and that the benefits might merely be alternate proofs of things we have proved via other means. I guess what the comments here are saying is the way to start is to start (with a new definition, and then the theorems which use it could be proved gradually).

But this might be waiting for a volunteer to take it on (could be future me - I'm not ruling anything out - but also might not be).

[digama0]

I think the simplest thing to do would be option (2), because most existing theorems would not have their statements be changed at all so less things would break, and it's obviously a lot less work than duplicating everything + relating two definitions. I don't think you need to change the reasoning of these proofs to actually work with the modulus of convergence. AFAICT geolim will "just work" without any proof changes, and in fact most of the chain of lemmas leading up to it as well; climsqz2 handles the definition directly but it would just be a quantifier interchange there and in most other places.

divcnv is interesting because it reveals an issue in the definition I suggested: I said you could use E. g : RR+ --> ZZ but actually intuitionistic logic has some trouble constructing such functions, and divcnv is using arch to get the integer, which is intrinsically nonconstructive. To fix this I think you should use E. g : NN --> ZZ with the property that for all n the series above g(n) is within 1/n of the value (which matches the definition in ax-caucvg). This will of course make divcnv particularly easy, but you can also prove that it is equivalent to having a function g : QQ+ --> ZZ like was done in the HoTT book.

Basically, my claim is that with this route the whole tower of theorems doesn't need to be torn down because all those theorems are still true - I can't find any that aren't - so only those that interact directly with the definition of convergence need to be updated. I can make a precise list later but I would estimate somewhere in the range of 20 theorems.

[jkingdon]

I think the simplest thing to do would be option (2), because most existing theorems would not have their statements be changed at all so less things would break, and it's obviously a lot less work than duplicating everything + relating two definitions.

I wouldn't get too hung up about option 2 versus option 3 (iset.mm has done both in different contexts) but instead focus on how many theorems have to change (in both statement and in proof). Either a separate definition or redefinition has the potential to save certain kinds of work but ultimately you need to get to the same place, of figuring out how all the things you want to prove can follow from the alternative definition. In particular, if the same proof works unmodified with either definition, then copying it over in the case of option 3 is mechanical easy work.

divcnv is interesting because it reveals an issue in the definition I suggested: I said you could use E. g : RR+ --> ZZ but actually intuitionistic logic has some trouble constructing such functions, and divcnv is using arch to get the integer, which is intrinsically nonconstructive. To fix this I think you should use E. g : NN --> ZZ with the property that for all n the series above g(n) is within 1/n of the value (which matches the definition in ax-caucvg).

Ah, maybe that's what the 1/n is doing in https://en.wikipedia.org/wiki/Modulus_of_convergence (it somehow creeps in between the "essentially" in the introductory paragraph and the more formal definition further down).

This will of course make divcnv particularly easy, but you can also prove that it is equivalent to having a function g : QQ+ --> ZZ like was done in the HoTT book.

Hmm, if we are talking about https://us.metamath.org/ileuni/cauappcvgpr.html and the HoTT book theorems on Cauchy approximations which it cites, I never did figure out how to get those to work. (That is, cauappcvgpr is unused and our actual development of completeness is from https://us.metamath.org/ileuni/caucvgprpr.html ).

Perhaps this is my other reason for trying to describe the issues as I understand them but not taking them on myself. Most of the work which went into making https://us.metamath.org/ileuni/ax-caucvg.html was not especially natural for me, and I'm not sure I'd make especially fast progress at a new convergence definition or come up with the most pleasing results. If anyone does want to work on this and has questions or concerns about getting this accepted into iset.mm, let's keep talking - I might have some thoughts but the bottom line is that I hope whatever conventions or directions we have enable this kind of work rather than act as a barrier.

I would estimate somewhere in the range of 20 theorems [need to be updated]

LOL maybe that's the gap in perceptions - whether 20 sounds like a small number or a big one!

[digama0]

I would estimate somewhere in the range of 20 theorems [need to be updated]

LOL maybe that's the gap in perceptions - whether 20 sounds like a small number or a big one!

Note that I mean 20 actual metamath $p statements, not 20 high level theorems (with 5 lemmas each). 20 lemmas is comparable to the size of most single PRs, so I wouldn't say it is a very large number. (But I will do a more precise count later rather than just estimating.)

Hmm, if we are talking about https://us.metamath.org/ileuni/cauappcvgpr.html and the HoTT book theorems on Cauchy approximations which it cites, I never did figure out how to get those to work. (That is, cauappcvgpr is unused and our actual development of completeness is from https://us.metamath.org/ileuni/caucvgprpr.html ).

Well, I was just referring generally to the strategy of using positive rational numbers for epsilon instead of 1/n or positive reals. The fact that you don't need to take inverses makes it a bit cleaner of a statement, although probably 1/n is still easier in many cases.

[digama0]

Okay here's the actual list. Unfortunately 20 theorems was an underestimate. These refactors have a tendency to be like containing a wildfire, you think you have them all and then one thing is off and a whole other section of theorems is touched.

+ df-clim
- climrel
+ clim
- climcl
+ clim2
- climshftlemg
+ clim2c
+ clim0
- climi
- climeq
+ clim0c
- climconst
+ 2clim
+ climcn1
+ climcn2
- climsqz
- climsqz2
- climrecvg1n
- climabs0
- serf0
- divcnv
- mertensabs
+ climcn1lem
- climcncf (1)
- climadd
- climmul
- climsub
- climabs
- climcj
- climre
- climim

There are 31 theorems in this list. The ones with + have had their statements changed, and all of their direct dependencies are in the list; the ones with - have their proofs changed due to a dependency change.

(1): Theorem climcncf reveals that ~~> connects to -cn->, so now we have to ask whether to change -cn-> as well. There is an analogous modification you can make to -cn-> to define "strong continuity"; if you don't change the definition then climcncf does not hold and you need an alternate route to get the direct dependencies.

Changing df-cncf looks like this:

+ df-cncf
+ cncfval
- cncfrss
- cncfrss2
+ addcn2
+ elcncf
+ subcn2
+ elcncf2
- cncff
- elcncf1di
- rescncf
+ cncfmet (2)
- cncfi
- cncffvrn
- abscncf
- recncf
- imcncf
- cjcncf
- mulc1cncf
- cncfco
- cdivcncfap
- mulcncf
+ cncfcncntop
+ cncfcn1cntop
- cnlimcim (3)

An additional 25 theorems. We have two additional notes:

(2): cncfmet relates -cn-> to Cn, and here we have no choice, Cn cannot be modified and it simply does not hold with "strong continuity". The analogue of strong continuity for topological spaces requires fixing a basis and then a "continuity witness" is a function from the codomain basis to the domain basis (i.e. "forall epsilon there is a delta") with the appropriate containment relation. It's a very different theory and probably not one you want to get into at the moment.

(3): cnlimcim implicates limCC as well. Since this one is over CC we may consider modifying it to the strong variant, which entails the following 10 additional theorems:

+ df-limced
- limcrcl
- limccl
+ ellimc3ap
- limcdifap
- limcimolemlt
- limcimo
- limcresi
+ cnplimcim (4)
- cnlimcim

(4): This one implicates CnP, which has a similar issue as Cn, the topological notion can't be changed so this one is no longer true with the strong limCC.

So where are we left? In total I have listed 66 theorems, which I would definitely classify as a "large" refactor, although one could cut it off at some of the listed intermediate points. I won't blame you for not wanting to take this on, although I do think that in the long run you will need the notion of strong convergence, strong continuity etc because it is needed to prove theorems without going back to the primitive definitions all the time (and in fact, this list is as large as it is in part because there are a lot of references to the primitive definition!).

[jkingdon]

Thanks for making that list!

So where are we left?

Well, I don't know what thoughts anyone else is having, but my reaction is that we need to keep both definitions around. This is partly due to the size of the task of changing anything, partly due to facilitating comparisons with set.mm (which can have practical and educational benefits), and perhaps most convincingly because there is a mathematical reality here as expressed in statements like "This one implicates CnP, which has a similar issue as Cn, the topological notion can't be changed so this one is no longer true with the strong limCC". We can express ideas like this formally at least in the sense of having the theorem with weak limCC but not strong limCC or whatever form it takes.

I do think that in the long run you will need the notion of strong convergence, strong continuity etc

I'm sure you are able to see ahead farther than I can on this. I'm really not all that far up the learning curve of understanding what prerequisites there are for https://us.metamath.org/mpeuni/dvcnp2.html or some replacement thereof which is sufficient to prove https://us.metamath.org/mpeuni/pire.html (just to pick a concrete example of something which in set.mm uses a bunch of these continuity theorems).

[jkingdon]

This might be too vague of a hunch to lead anywhere but I can't help but wonder whether there's some connection to "Is there a Dedekind real which is not a Cauchy real?" at https://mathstodon.xyz/@andrejbauer/111013136967095323 . Perhaps I'm just overreacting to the presence of sequences and countable choice both places, though.