Weierstrass M-test

Stream: Is there code for X?

[Chris Birkbeck]

Do we have the Weierstrass M-test in mathlib? Or maybe in some not yet PR'ed repo? The specific result I want is this: https://en.wikipedia.org/wiki/Weierstrass_M-test

[Kevin Buzzard]

Perhaps you should look for some more general result involving functions taking values in some locally convex normed topological vector space ;-) (this is not a serious comment). I can't find it in the docs even though to be honest this does look like the kind of thing which we will have somewhere, nowadays.

[Chris Birkbeck]

Yes this definitely feels like its something that might already be in mathlib, in the maximum level of generality possible, under a different name.

[Kevin Buzzard]

Why not just prove it and PR it :-) Note that in the Wikipedia page A really is just a random type as opposed to anything with a real or topological structure.

[Chris Birkbeck]

Yes, well I was thinking of doing just that. But I thought I'd first check if being lazy is an option :)

[Kevin Buzzard]

I think it could be -- we just need to wait for someone who knows that part of the library.

[Damiano Testa]

Maybe I am misunderstanding, but a combination of docs#nnreal.summable_of_le and docs#summable.of_abs could work?

[Damiano Testa]

(Although, I have not yet found something about uniform convergence.)

[Chris Birkbeck]

Yes the summable part is very doable. Its the uniform part which I can't really find. But summable_iff_vanishing_norm combined with metric.tendsto_uniformly_iff (+ other junk) might be enough to reproduce the wikipedia proof.

[Damiano Testa]

Ok, I was not really sure about which parts were you looking for.

[Heather Macbeth]

@Chris Birkbeck, I think you could just apply docs#summable_of_norm_bounded to the Banach space of continuous functions with the uniform norm, docs#bounded_continuous_function.normed_group.

[Chris Birkbeck]

Thank you for the suggestion. I'd managed to prove it before seeing this, but I guess the normed_group proof may be nicer. I'll think about it and see if I can make it work.