An introduction to statistical modelling semantics with higher-order measure theory
SPLV: The 4th Scottish Programming Languages and Verification Summer School
Ohad Kammar 11-16 July 2022
The last few years have seen several breakthroughs in the semantic foundations of statistical modelling. In this course, I will introduce one of these approaches — quasi-Borel spaces. We will review and develop a semantic tool-kit for measure theory using higher-order functions. The course will be accompanied by exercises and tutorials, allowing you to develop a working knowledge and hands-on experience.
Course materials
Slides
-
All slides
(updated with corrections)
Lectures
1-2 (video unavailable unfortunately)
Lectures
3-4 (video)
See the Marseille course for additional content and videos.
Exercise sheet (under development)
-
Context and background
Doing all of these exercises is too much for the course, the goal is to learn something new, or — if you already know this material — help someone else learn something new.
-
Borel
set basics: introductory exercises if you’ve never worked with Borel
sets, or looking for a refresher.
Measurable
spaces and functions: exercises exploring the structure of
measurable spaces and measurable functions.
Basic
category theory: use these exercises to improve your category
theory.
Aumann’s
theorem: consequences of and related concepts to Aumann’s theorem on
the inexistence of measurable function-spaces.
Sequences:
examples of higher-order measure theory using sequences.
-
Quasi-Borel
spaces: first acquaintance with quasi-Borel spaces.
Qbs
construction: space combinators — you may want to spread these
exercises over several sittings.
Borel
subspaces: measurable subsets in a quasi-Borel space.
-
Function
spaces: practice the definition of the function space of two qbses,
with the Borel subsets and random element spaces.
Type
structure: use type-formers to put spaces together and form more
complex spaces.
Standard Borel spaces (under development): use measurability-by-type to
construct standard Borel spaces.
-
Measures: introductory exercises if you’ve never worked with measures
before.
Lebesgue integration: the definition of the Lebesgue integral.
Randomisable measures: the class of measures we will work with.
-
Random variable spaces: definition and basic properties of the Lebesgue
spaces.
Geometry of random variable spaces: basic geometric and topological
properties of Lebesgue spaces.
Conditional expectation: existence and almost-certain uniqueness of
Kolmogorov’s conditional expectation.
-
More
on the Borel hierarchy: a guided tour of the proof of Aumann’s
theorem.
Aumann’s
theorem for Lebesgue measurablity: extending Aumann’s theorem from
Borel measurable functions to Lebesgue measurable functions.