Infinite products

Stream: mathlib4

[Mitchell Lee]

There's a folder in mathlib called Mathlib.Topology.Algebra.InfiniteSum that defines infinite sums in an (additive) commutative topological monoid.

It would be nice, I think, to have a similar notion for infinite products in a (multiplicative) commutative topological monoid. This would, for example, make it easier to state a result like docs#EulerProduct.eulerProduct. (I know that technically there is already Additive.toMul (∑' a, Additive.ofMul (f a)), but I hope I do not need to explain why this is undesirable.)

I would be happy to help make this happen. What would be the best approach?

[Yaël Dillies]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/infinite.20product.20clash.20with.20type.20product/near/326028832

[Yaël Dillies]

See also !3#18405

[Mitchell Lee]

I see. Thank you for the links.

I will say that I would be inclined to directly "multiplicativize" the existing infinite sum code, rather than require that every term of the product is a unit. After all, the definition of a convergent infinite sum doesn't require that every term has a multiplicative inverse, or is even cancellable. If you want things like $\prod_{n \in \mathbb{N}} \frac{1}{2}$ not to exist, then you can carry out the product in $\mathbb{R}^\times$ instead of $\mathbb{R}$.

[David Loeffler]

@Mitchell Lee What you are suggesting (naively multiplicativizing the existing definitions for sums) might seem logically tidy, but unfortunately does not match the way that infinite products get used in the established mathematics literature, and there was a consensus in the previous thread that we should not follow this path.

[Mitchell Lee]

From David Loeffler:

If R is a topological ring, then I think we should define "convergence" of a product valued in R to mean that every term of the product is a unit in R, and the convergence holds be w.r.t. the morally-correct topology on $R^\times$, which is the one induced by its embedding into $R \times R$ via $t \mapsto (t, 1/t)$.

Is it not true that a product $\prod_{x \in I} f(x)$ converges in this stronger sense if and only if it converges in the naive sense (i.e. the filter of finite partial products converges) and the value of the product is a unit?

[David Loeffler]

As pointed out by others in the thread, this is probably not the right definition, and it is better to allow finitely many non-unit terms.

[Mitchell Lee]

I cannot see that suggestion in the thread. The closest thing I can see is the suggestion of Sébastien Gouëzel, which is to require that every product of all but finitely many of the terms converges "in the naive sense" (of the filter of finite partial products converging). It is not obvious to me whether this is equivalent to the statement that there are finitely many non-unit terms and the product of the unit terms converges in the "morally correct" topology.

This definition excludes $\prod_{n = 0}^\infty (2^n - 1)$, which probably shouldn't be considered to converge, without excluding $\prod_{n = 1}^\infty \left(1 - \frac{1}{n^2}\right)$, which probably should be considered to converge.

But then, I think if we decide to adopt this definition, there is no reason that we couldn't use the same thing for infinite sums.

[Mitchell Lee]

Overall, though, here is my opinion: there is not actually a consensus in the literature about what it means for an infinite product to converge, and I don't see what horrible thing is going to happen if we just decide that $\prod_{n = 0}^\infty (2^n - 1) = 0$.

[Mitchell Lee]

You also gave the example of $\prod_{n} p$ in $\mathbb{Z}_p$. Similarly, I can't see what's wrong with saying that this product is $0$ if carried out in $\mathbb{Z}_p$, and it doesn't exist if carried out in the cancellative monoid $\mathbb{Z}_p \setminus \{0\}$. This is what the naive "multiplicativization" of the current definition of infinite sums already does.

But more importantly, I think no one would ever consider such a product, so it doesn't really matter whether we say it's $0$ or not.

[Mario Carneiro]

David Loeffler said:

As pointed out by others in the thread, this is probably not the right definition, and it is better to allow finitely many non-unit terms.

Can you point more specifically to where this is said? I can only see you making this claim in the earlier thread.

[Mario Carneiro]

Note that any weirdness that arises for infinite products also arises for infinite sums, because we can take sums over topological monoids with a $-\infty$ element in the domain

[David Loeffler]

Mario Carneiro said:

Can you point more specifically to where this is said? I can only see you making this claim in the earlier thread.

The suggestion came from Sebastian: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/infinite.20product.20clash.20with.20type.20product/near/326054526

[David Loeffler]

If you specialise to the case of values in a field, then this is also (close to) the notion of "convergence" used in the statements scanned from a textbook that Yakov was uploading (the difference being that this text was using a different, order-dependent notion of convergence for the non-vanishing tail product). So it was not just me who was arguing for a notion of product convergence other than the naive multiplicativization of the sum definition.

[Mitchell Lee]

Yes; as I said, the suggestion from Sebastian is different from the one you made.

[David Loeffler]

Mitchell Lee said:

Overall, though, here is my opinion: there is not actually a consensus in the literature about what it means for an infinite product to converge, and I don't see what horrible thing is going to happen if we just decide that $\prod_{n = 0}^\infty (2^n - 1) = 0$.

One thing you lose by doing this is that the standard and widely-used lemma that for a sequence of non-negative reals $a_n$, the product $\prod(1 + a_n)$ converges iff $\sum a_n$ converges. I think it would be unfortunate to adopt a notion of product convergence for which this lemma does not hold.

[Mitchell Lee]

You don't lose that lemma, though.

[David Loeffler]

Mitchell Lee said:

You don't lose that lemma, though.

I'm pretty sure $\sum_{n \ge 1} (2^n - 2)$ doesn't converge...

[Mitchell Lee]

That's not a series of nonnegative real numbers

[Mitchell Lee]

Okay, I see your point, that maybe you want it with "eventually nonnegative"

[David Loeffler]

Well, I want convergence of $\prod_{n \in \mathbb{N}} a_n$ to imply convergence of $\prod_{n \in \mathbb{N}} a_{n + k}$ for any $k$.

[Mitchell Lee]

Okay, then we should use Sebastian's suggestion. But if we do that, we should do the same thing for additive.

[David Loeffler]

I also think it's desirable that $\prod_{n \in \mathbb{N}} a_n^{-1}$ should converge iff $\prod_{n \in \mathbb{N}} a_n$ does. That's not true with Sebastian's definition: one would need a hybrid of Sebastian's definition and the one from Yakov's textbook clipping.

[Sébastien Gouëzel]

The conclusion I had arrived on my side is the following: The simplest and wisest thing to do is probably just to (1) multiplicativize the current definitions, as it will give a reasonable definition for many cases (with the drawback you're pointing that convergence of $\prod_{n \in \mathbb{N}} a_n$ does not imply convergence of $\prod_{n} a_{n+1}$, but I'm not sure it will be a real pain). And then (2) add a second layer on top of this one, if it looks really useful, implementing a more complicated definition but with better properties in some cases.

[Mitchell Lee]

Sorry for getting your name wrong

[Sébastien Gouëzel]

Don't worry about my name, I'm used to every possible variation :-)

[Sébastien Gouëzel]

The advantage is that (1) can be done now, and (2) can be done later if/when needed.

[Sébastien Gouëzel]

David Loeffler said:

As pointed out by others in the thread, this is probably not the right definition, and it is better to allow finitely many non-unit terms.

No, this is bad, because when you additivize this then you get that in NNReal there is essentially no convergent sum (as the only element which is a unit for addition is zero...)

[Mitchell Lee]

Yes, I think it would make sense to have multiple definitions. However, I would not want to select any more than two of the five different things that have been suggested.

I do not think that "$\prod_{n \in \mathbb{N}} a_n^{-1}$ converges if and only if $\prod_{n \in \mathbb{N}} a_n$ does" is essential. What's wrong with "$\prod_{n \in \mathbb{N}} a_n^{-1}$ converges to a nonzero number if and only if $\prod_{n \in \mathbb{N}} a_n$ does"?

[David Loeffler]

Sébastien Gouëzel said:

No, this is bad, because when you additivize this then you get that in NNReal there is essentially no convergent sum (as the only element which is a unit for addition is zero...)

This argument is only conclusive if you also require that whatever definition we use for products also has to give a good result for sums under additivization; and I don't think that's a "given" here, is it? It's one of the many properties that would be nice to have, but we can't have all the "nice-to-haves" at the same time, and we're trying to find the best compromise.

[David Loeffler]

That said, I think Sebastien's argument is a very convincing one – that we should try out the naive multiplicativization of the existing definition, and see if it works well in practice. If it does turn out to be impossibly painful to work with, then that experience will help us to make an informed judgement on what we should go for instead.

[Mitchell Lee]

Well, one could make the same remark about the multiplicative monoid of all real numbers that are greater than or equal to 1. Are you just not allowed to take infinite products in that monoid?

[Sébastien Gouëzel]

David Loeffler said:

This argument is only conclusive if you also require that whatever definition we use for products also has to give a good result for sums under additivization.

Yes, absolutely. The big advantage of this approach is that, in this case, you just need to write everything once in the product case, and you get the sum case through to_additive. While otherwise you need to write everything twice. I am all for minimizing the pain :-)

[Yaël Dillies]

David Loeffler said:

That said, I think Sebastien's argument is a very convincing one – that we should try out the naive multiplicativization of the existing definition, and see if it works well in practice. If it does turn out to be impossibly painful to work with, then that experience will help us to make an informed judgement on what we should go for instead.

In fact that's exactly the reasoning I had when I made !3#18405 :smile:

[Mitchell Lee]

This is kind of a contrived example, but I think it isn't totally frivolous either.

In the ring of real numbers, we have $\prod_{n \geq 0} \left(1 + 2^{-2^n}\right) = 2$. Each term of the product lies in the subring of dyadic rationals, as does the product itself. So I should be able to do the same product in that ring, too. But in the ring of dyadic rationals, this is a product of infinitely many nonunits.

[David Loeffler]

I concede that requiring only finitely many non-unit terms does not work well when the target space is not a topological field (but I do claim that this special case is quite an important one).

[Mitchell Lee]

Yes, I think that topological fields are the most important case. However, in this case, there is not much that needs to be done. One of the most common definitions of infinite product convergence in the mathematical literature is that the finite partial products converge to a nonzero element. In a topological field, this notion of convergence is easily recoverable from the naive notion in two different ways: you could either carry out the product in the unit group, or you could carry out the product and then require that the answer is nonzero.

I think the naive notion (i.e. the direct multiplicativization of what we use for sums) is our best option.

Then, in the specific case that $R$ is a complete normed ring, we can say that a product $\prod_{x \in X} f(x)$ converges absolutely if the sum $\sum_{x \in X} \|f(x) - 1\|$ converges. This implies convergence in the naive sense, and the lemma you mentioned earlier is true essentially by definition. It also has nice properties like being preserved by continuous homomorphisms. I much prefer this to trying to reason about which terms of the products are allowed to be nonunits.

[Yakov Pechersky]

Sorry to post in the middle of a complex discussion... One of the reasons I paused on formalization of that infinite products text is because of a lot of obstacles that are mentioned here. One in particular was that I couldn't come up with a satisfactory definition that allowed for all infinite products on the unit interval (a monoid with zero) to converge or diverge to zero.

[Mitchell Lee]

(Sidenote: that textbook you showed us was specifically trying to define conditional convergence of the product of a sequence. That definition should be added to Mathlib eventually, but I think we should start by defining unconditional convergence of an arbitrarily indexed product.)

[Antoine Chambert-Loir]

I don't know what litterature you're referring to, but let me recall that Bourbaki, General Topology, uses the mul-version the actually present add-version.
While I know that there are contexts where more stringent hypotheses are assumed, with more stringent consequences, It would be very awkward to have another definition.

[David Loeffler]

@Antoine Chambert-Loir I looked in Bourbaki's "General Topology" and did not find that definition, can you let me know where it can be found in the book?

[David Loeffler]

Chapter 3 of that book contains extensive discussion of sums in topological groups, and there is a brief throwaway remark that the definitions work for monoids too. But that is not the definition that is used later on in the same text, e.g. in Ch 4 sect 6 we read the following:

An infinite product of finite non-zero real numbers is said simply to be convergent if it is convergent in $\mathbf{R}^*$; its value is then a finite non-zero real number.

So for Bourbaki, $\prod_{n \in \mathbb{N}} (1 - 1 / (n+1))$ is not convergent, and so their notion of "convergence" does not agree with their definitions for monoids applied to the multiplicative monoid of $\mathbb{R}$.

[Antoine Chambert-Loir]

I'm sorry to disagree. In chapter 3, page 37, remarque 3 (French edition), they say that the definitions they gave for summable families apply to multiplicative monoids. The example you give is a case of a family of real numbers which happen to live in a submonoid (nonzero real numbers) which converges in the ambient monoid but not in the smaller one.

[Antoine Chambert-Loir]

They also use that definition for power series (Algebra, chapter 4, §4), although the only case where they prove a product $\prod (1+f_i)$ is multipliable is the case where the family $\sum f_i$ is summable.

[David Loeffler]

@Antoine: you appear to be disagreeing with your own chosen source. Please see the quote I provided above from Bourbaki ch 4 sect 6.

[Antoine Chambert-Loir]

In Bourbaki's language, the use of the adverb “simply” means that they know it's not the definition, but it's easier to pretend it is.

[David Loeffler]

Interesting. I can't believe there are people who think Bourbaki constitutes a model for good mathematical writing.

[Antoine Chambert-Loir]

Who said that?

[David Loeffler]

I've seen "simply" used to mean "this isn't the definition, but it is equivalent to the definition and more convenient". I've never seen "simply" to mean "this is logically incompatible with the definition but we somehow overlook the inconsistency".

[Antoine Chambert-Loir]

Maybe the text suffers from the translation here, because the French « simplement » doesn't imply that it is equivalent. In fact, the whole of chapter 4, §4, plays with this kind of conventions:

• n°1 and n°2 are about summable families “in $\mathbf R$;
• n°4 about multipliable families “in $\mathbf R^*$;
• n°5 is about summable families “in $\overline{\mathbf R}$;
• n°6 is about convergent series “in $\mathbf R$”.

[Antoine Chambert-Loir]

I think what is needed is the way of phrasing the existence of a limit in a submonoid, without having to coerce everything from scratch.

[Mitchell Lee]

Here is my interpretation of the Bourbaki text: the product $\prod_{n} \frac{1}{2}$ converges when carried out in $\mathbb{R}$, and it does not converge when carried out in $\mathbb{R}^*$. However, when we say that a product of nonzero real numbers "converges" without specifying the monoid, we mean that it converges in $\mathbb{R}^*$.

This is 100% compatible with the naive multiplicativization. As I said, if you don't want $\prod_{n} \frac{1}{2}$ to exist for some reason, just do the product in $\mathbb{R}^*$.

[Mitchell Lee]

Moreover, there is no need to even coerce all the terms to the multiplicative group, if you find that to be too annoying (even though it is exactly as annoying as having to prove that all the terms are nonzero every time you want to even write down a product). A product $\prod_{x \in X} f(x)$ exists in $\mathbb{R}^*$ if and only if it exists in $\mathbb{R}$ and its value is nonzero.

[Mitchell Lee]

Finally, as I understand it, part of the design philosophy of mathlib is to let users write down expressions like $\prod_{n} \frac{1}{2}$, even if some people consider them illegal. We even have 1 / 0 in Lean, and that causes a lot more problems than $\prod_{n} \frac{1}{2}$ ever could. We can solve these problems by adding the appropriate hypotheses to theorems involving infinite products, rather than simply forbidding users from taking products like $\prod_{n} \frac{1}{2}$.

[Mitchell Lee]

(By the way, I think the word "simply" in the Bourbaki text is merely highlighting the fact that "convergent" is a simpler phrase than "convergent in $\mathbb{R}^*$". In formalized mathematics, this is irrelevant, because you would always specify the monoid.)

[Mitchell Lee]

Anyway, shall I get started?

[Mitchell Lee]

Okay, here it is: #11733

[Mitchell Lee]

Thanks Yaël Dillies for the review; I've made the requested changes.

[Mitchell Lee]

Arbitrarily indexed products are on master now. I appreciate Yaël Dillies and Sébastien Gouëzel so much for helping with this. They caught a lot of my mistakes.

There are a few directions that are now opened up.

• Mathlib/Analysis/Normed/Group/InfiniteSum.lean is still not multiplicativized at all. This might be a bit more annoying because the correct multiplicativization of (for example) Summable.of_norm will involve both a sum and a product. I still think @[to_additive] should be able to handle it, though.
• Mathlib/NumberTheory/EulerProduct/Basic.lean uses an ad-hoc implementation of infinite products. More specifically, it takes a partial product over all primes below N and then takes the limit as N goes to infinity. I think that by using the new implementation of infinite products, these results in this file can be strengthened (to prove unconditional convergence of the Euler product, rather than just conditional convergence) and made easier to use.
• As David Loeffler mentioned, it is likely that we will want to implement a stronger notion of multipliability at some point. (I believe that this should complement the current definition rather than replacing it.) Earlier in this thread, I suggested "absolute multipliability" for products whose terms lie in a normed ring: we say $f$ is absolutely multipliable if $\sum \| f(x) - 1 \|$ exists. It may be worth thinking about this or other possible conditions.

[Michael Stoll]

Mitchell Lee said:

Arbitrarily indexed products are on master now. I appreciate Yaël Dillies and Sébastien Gouëzel so much for helping with this. They caught a lot of my mistakes.

There are a few directions that are now opened up.

• (...)
• Mathlib/NumberTheory/EulerProduct/Basic.lean uses an ad-hoc implementation of infinite products. More specifically, it takes a partial product over all primes below N and then takes the limit as N goes to infinity. I think that by using the new implementation of infinite products, these results in this file can be strengthened (to prove unconditional convergence of the Euler product, rather than just conditional convergence) and made easier to use.
• (...)

This is on my to-do list.

[Michael Stoll]

The module docs of Mathlib.Topology.Algebra.InfiniteSum.NatInt should be adapted to mention products as well :smile:

[Michael Stoll]

I will need something along the lines of "f : ℕ → R (with, say, [NormedCommRing R] [CompleteSpace R]) is multipliable if f n = 1 + g n for all n and (‖g ·‖) is summable". Do we have this somewhere?

[Michael Stoll]

@Mitchell Lee ? :up:

[Mitchell Lee]

Michael Stoll said:

The module docs of Mathlib.Topology.Algebra.InfiniteSum.NatInt should be adapted to mention products as well :smile:

#12019

[Mitchell Lee]

Michael Stoll said:

I will need something along the lines of "f : ℕ → R (with, say, [NormedCommRing R] [CompleteSpace R]) is multipliable if f n = 1 + g n for all n and (‖g ·‖) is summable". Do we have this somewhere?

We don't have it yet. I think we should actually have this definition somewhere: f is absolutely multipliable if ‖f · - 1‖ is summable. Then we should prove that in a complete normed ring, absolutely multipliable implies multipliable.

[Mitchell Lee]

Then we would have two notions of product convergence: one which is very permissive, and one which is better behaved with respect to removing or adding terms and better matches the definition we saw in that textbook.

[Michael Stoll]

Michael Stoll said:

Mitchell Lee said:

Arbitrarily indexed products are on master now. I appreciate Yaël Dillies and Sébastien Gouëzel so much for helping with this. They caught a lot of my mistakes.

There are a few directions that are now opened up.

• (...)
• Mathlib/NumberTheory/EulerProduct/Basic.lean uses an ad-hoc implementation of infinite products. More specifically, it takes a partial product over all primes below N and then takes the limit as N goes to infinity. I think that by using the new implementation of infinite products, these results in this file can be strengthened (to prove unconditional convergence of the Euler product, rather than just conditional convergence) and made easier to use.
• (...)

This is on my to-do list.

#12055 is a first step, which should make it easy to talk about convergence in the sense of tprod (we consider sets of natural numbers with prime factors in any given finite set, not necessarily all primes below some bound).

[Michael Stoll]

#12161 deals with the TODOs in Mathlib/NumberTheory/EulerProduct/Basic.lean.