E-values

Stream: Is there code for X?

[Josha Dekker]

Do we have e-values in Mathlib? e-values are a relatively recent alternative to p-values for hypothesis testing with nice properties (e.g. they behave well under optional stopping)

[Rémy Degenne]

We don't have a definition of e-values. It's super easy to write one, since it's simply non-negative random variables with expectation less than 1 wrt a particular measure, but we don't have it. That obviously also means that we don't have anything about them.

I recently added a few things about the log-likelihood ratio (docs#MeasureTheory.llr), which for probability measures is an e-value (and abstracting away the particular definition of the LLR to consider more general random variables is one of the motivations of e-values Wouter Koolen mentioned last time we talked about it). I did that as preparation for a project about information divergences and hypothesis testing.

[Josha Dekker]

Thank you! Good to know, I’ll keep it in mind if I’m looking for something to formalize in probability!