Tail expectation formula for L1 random variable #5130

Job	Run time
rocq-elpi	49s
rocq-core	50s
coq-elpi	48s
stdlib	50s
coq	46s
mathcomp-bigenough	50s
mathcomp-finmap	55s
hierarchy-builder	49s
mathcomp	55s
mathcomp-classical	3m 9s
mathcomp-analysis-single	18m 16s
mathcomp-reals	2m 12s
mathcomp-analysis	17m 41s
mathcomp-reals-stdlib	2m 52s
mathcomp-experimental-reals	3m 24s
mathcomp-analysis-stdlib	34m 48s
	1h 29m 54s

Provide feedback