mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(probability/tail_prob): the tail probability formula

Open kex-y opened this issue 3 years ago • 1 comments

This PR adds the tail probability formula which is needed for Doob's Lp inequality.

Open in Gitpod

kex-y avatar Jun 16 '22 15:06 kex-y

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

kex-y avatar Jun 17 '22 09:06 kex-y