Zulip Chat Archive

Stream: Brownian motion

Topic: Uniform Integrability of Constant Sequence in Lp when p = ∞


Jack McCarthy (Nov 19 2025 at 05:41):

I'm currently working on the theorem uniformIntegrable_of_dominated_singleton, and running into trouble trying to prove the uniform integrability of a constant sequence fun _ ↦ Y where Y is MemLp. The existing theorems in mathlib to prove something like this, for example uniformIntegrable_const or unifIntegrable_const require the additional hypothesis that p ≠ ∞, which we do not have here. You can find my work in progress in PR #293.

Can anyone suggest how to proceed in the case when p = ∞? Or, alternatively, would it be alright to add the hypothesis p ≠ ∞ to the theorem, and then refactor the uses of uniformIntegrable_of_dominated_singleton to include this condition?

Etienne Marion (Nov 19 2025 at 06:30):

You have to assume that p is finite yes.

Etienne Marion (Nov 19 2025 at 06:35):

Actually I am not sure uniform integrability even makes sense when p is infinite, I think one might be able to prove that if one of the function is non zero then the sequence cannot be uniformly integrable if p is infinite.

Jack McCarthy (Nov 19 2025 at 06:46):

Ok thanks for confirmation, I will add the assumption that p is infinite

Yongxi Lin (Aaron) (Nov 19 2025 at 10:09):

Etienne Marion said:

Actually I am not sure uniform integrability even makes sense when p is infinite, I think one might be able to prove that if one of the function is non zero then the sequence cannot be uniformly integrable if p is infinite.

How about measures with atoms? If your probability space Ω is a singleton, then any bounded collection of random variables is uniformly integrable for p = ∞.

Etienne Marion (Nov 19 2025 at 10:33):

Yes I did not intend to make a precise statement. It's just that if the function is not zero ae it is bounded below on a set of positive measure. If this set contains measurable sets of arbitrary small and positive measure, then you don't get uniform integrability. The fact that a singleton might not be uniformly integrable I think suggests that this notion is not interesting when p is infinite. Actually in the project we will most likely not care about p ≠ 1 I think, because p=1 is the right assumption to have nice properties of martingale (eg convergence in L1), and for convergence in Lp it suffices to be bounded in Lp I think (at least it's true in the discrete case)?


Last updated: Dec 20 2025 at 21:32 UTC