On July 31, 2024 at 16:00 EEST, Morenikeji Neri (University of Bath) will give a talk in the Proof Mining Seminar.
Title: Proof mining and probability
Abstract:
Due to previous ad hoc case studies, the insight was made that a significant proportion of results in probability theory (and finite measure theory, in general) made use of infinite unions and sigma additivity in a very sparing way, allowing for a formalisation amenable to bound extraction, in the style of the classical proof mining metatheorems. This talk will discuss aspects of recently developed formal systems stemming from this perspective. While these systems entail many subtle details and features, we shall focus on those that allow us to discuss their key achievements. This includes a novel extension of Bezem’s majorizability that explains the uniformities in the extracted bounds of previous case studies and the formalisation of a strategy that transfers quantitative deterministic results to their corresponding probabilistic analogues. This is joint work with Nicholas Pischke.
Google Meet link: https://meet.google.com/jpw-hrwe-evu