Tail expectation formula for L1 random variable #83

Job	Run time
rocq-core	44s
mathcomp	51s
coq	47s
mathcomp-classical	2m 42s
mathcomp-analysis-single	14m 46s
mathcomp-reals	2m 2s
mathcomp-experimental-reals	3m 11s
mathcomp-reals-stdlib	2m 38s
mathcomp-analysis	13m 43s
ssprove	13m 57s
mathcomp-analysis-stdlib	13m 42s
mathcomp-infotheo	7m 21s
	1h 16m 24s

Provide feedback