Lévy-Steinitz Theorem

Stream: Is there code for X?

[Niels Voss]

Does the proof of the Lévy-Steinitz theorem, which states that the set of values that a series of vectors in ℝ^n can converge to is either empty or a subspace of ℝ^n, exist anywhere? Is there anyone working on it or its corollary, the Riemann Series Theorem?

[Jireh Loreaux]

I'm fairly certain we don't have it. Things in Mathlib about conditional convergence are pretty sparse.

[Niels Voss]

Is this something that would be accepted into mathlib if it were proven?

[Jireh Loreaux]

Sure. We just don't have it because in practice what you want most of the time is docs#tsum

[Antoine Chambert-Loir]

This is a fantastic theorem (as is its generalization to all lctvs — in the metrizable case, a necessary and sufficient condition to add is that the space be nuclear).
I am not sure mathlib has the 1D case, and that is already nice.

[Antoine Chambert-Loir]

Which proof scheme would you follow?

[Jireh Loreaux]

Antoine, what do you mean by nuclear? I know two different ideas associated to that term, but I don't think you're referring to either of them.

[Niels Voss]

Antoine Chambert-Loir said:

This is a fantastic theorem (as is its generalization to all lctvs — in the metrizable case, a necessary and sufficient condition to add is that the space be nuclear).
I am not sure mathlib has the 1D case, and that is already nice.

What is an LCTVS? Is it a locally convex topological vector space?

I am using the Peter Rosenthal proof here: https://sites.math.washington.edu/~morrow/335_17/levy.pdf. This proof seems to construct a lot of permutations by means of "choose vectors until a condition is met, then choose vectors until a second condition is met, then swap", so if you know another proof, I'd look into it.

[Niels Voss]

Are the generalizations to LCTVS significantly more difficult to prove? The proof I'm using only works on R^n, and I'm not sure how much I'd be able to understand the more abstract spaces

[Antoine Chambert-Loir]

I can't claim I understand it but it's not very long. It is geometry of Banach spaces.

[Niels Voss]

I think I might stick to just R^n (and by extension, all TVSes which are isomorphic to R^n). I only really know a little bit of point-set topology and basic linear algebra, and I haven't ever done any functional analysis, so I don't think I have the prerequisites for one of the more general version of the proof.

Out of curiosity though, where would a proof of this generalization be found? The Peter Rosenthal proof only works for finite dimensional spaces because it depends on induction over the dimension.

[Jireh Loreaux]

Jireh Loreaux said:

Antoine, what do you mean by nuclear? I know two different ideas associated to that term, but I don't think you're referring to either of them.

Nevermind, I've just realized what you meant, and actually that all these notions are basically equivalent.

[Antoine Chambert-Loir]

Here is the proof of Steinitz theorem fir nuclear spaces:

The Steinitz theorem on rearrangement of series for nuclear spaces
Wojciech Banaszczyk
Journal für die reine und angewandte Mathematik (1990)
Volume: 403, page 187-200

[Antoine Chambert-Loir]

https://eudml.org/doc/153193

[Antoine Chambert-Loir]

And the converse theorem :

Rearrangement of series in nonnuclear spaces,
Wojciech Banaszczyk
Studia Mathematica (1993)
Volume: 107, Issue: 3, page 213-222

https://eudml.org/doc/216030