Kexing Ying

icon indicating a website link kex-y.github.io icon indicating an email [email protected]

icon location Lausanne, Switzerland icon location PhD student in stochastic analysis at EPFL

Results 5 comments of Kexing Ying

feat(topology/algebra/infinite_sum): generalize `tsum_le_of_sum_range_le`

I'm not sure what structure will work here. My instinct is to use `tendsto_of_monotone` but that requires a `conditionally_complete_linear_order` which `ennreal` does not satisfy

feat(topology/algebra/infinite_sum): generalize `tsum_le_of_sum_range_le`

I tried a bit more but I can't find a nice form to state the theorem in so it's sufficiently general. I think I'll merge this for now. bors r+

feat(probability/independence): Kolmogorov's 0-1 law

I think this looks good! maintainer merge

feat(probability/tail_prob): the tail probability formula

This PR is somewhat superseded by #14424 I will make this PR dependent on it and obtain the result for integrals instead of lintegrals

feat(MeasureTheory): two lemmas on almost everywhere equality and positive lintegral

I think this looks good! maintainer merge