BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Etienne Marion (École Normale Supérieure de Lyon)
DTSTART:20260122T173000Z
DTEND:20260122T180000Z
DTSTAMP:20260420T025129Z
UID:LT2026/36
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/36/">
 Formalization of the Ionescu-Tulcea theorem in Mathlib</a>\nby Etienne Mar
 ion (École Normale Supérieure de Lyon) as part of Lean Together 2026\n\n
 \nAbstract\nWe describe the formalization of the Ionescu-Tulcea theorem\, 
 showing the existence of a probability measure on the space of trajectorie
 s of a Markov chain\, in the proof assistant Lean using the integrated lib
 rary Mathlib. We first present Markov kernels\, which are the objects of i
 nterest in this theorem. Then after giving a glimpse of the proof\, we exp
 ose the difficulties which arise when trying to formalize it\, and how the
 y were overcome.\n
LOCATION:https://researchseminars.org/talk/LT2026/36/
END:VEVENT
END:VCALENDAR