[Merged by Bors] - feat(measure_theory/function/uniform_integrable): add API for uniform integrability in the probability sense #12678
Conversation
JasonKYi
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
| (h : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0, 0 < C ∧ | ||
| ∀ i, snorm ({x | C ≤ ∥f i x∥₊}.indicator (f i)) p μ ≤ ennreal.of_real ε) : |
There was a problem hiding this comment.
Why do you use ennreal.of_real ε for ε real rather than define ε as an ennreal?
Also that property can be written as tendsto some_function_of_C at_top (nhds 0). Would we gain something by using the tendsto API? I am not sure it's worth changing.
There was a problem hiding this comment.
I used ennreal.of_real ε since I had used the same formulation for unif_integrable. I don't remember exactly why I used ennreal.of_real ε to define unif_integrable but I recall we needed \epsilon \ne \infty sometimes which taking epsilon to be real avoids.
There was a problem hiding this comment.
About the second comment. I think we will use the current formulation more than the tendsto version. If needed, we can always show that the two formulations are equivalent
There was a problem hiding this comment.
After some tests, I am convinced that this file and some statements of the egorov file would be simpler and better with ε : ennreal than with the current ennreal.of_real ε, but I will PR all those changes later. Let's keep the current formulation for now.
RemyDegenne
added
awaiting-author
JasonKYi
added
awaiting-review
|
bors r+ |
github-actions
bot
added
ready-to-merge
… integrability in the probability sense (#12678) Uniform integrability in probability theory is commonly defined as the uniform existence of a number for which the expectation of the random variables restricted on the set for which they are greater than said number is arbitrarily small. We have defined it in mathlib, on the other hand, as uniform integrability in the measure theory sense + existence of a uniform bound of the Lp norms. This PR proves the first definition implies the second while a later PR will deal with the reverse direction.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Uniform integrability in probability theory is commonly defined as the uniform existence of a number for which the expectation of the random variables restricted on the set for which they are greater than said number is arbitrarily small. We have defined it
in mathlib, on the other hand, as uniform integrability in the measure theory sense + existence of a uniform bound of the Lp norms.
This PR proves the first definition implies the second while a later PR will deal with the reverse direction.