A measurable space is a space equipped with a σ-algebra.

Propositional equality is `Decidable` for all elements of a type.

In other words, an instance of `DecidableEq α` is a means of deciding the proposition `a = b` is
for all `a b : α`.

A typeclass mixin for `MeasurableSpace`s such that each singleton is measurable.

A type `α` is countable if there exists an injective map `α → ℕ`.

The canonical type with one element. This element is written `()`.

`Unit` has a number of uses:
* It can be used to model control flow that returns from a function call without providing other
  information.
* Monadic actions that return `Unit` have side effects without computing values.
* In polymorphic types, it can be used to indicate that no data is to be stored in a particular
  field.

The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.

A measure `μ` is called a probability measure if `μ univ = 1`.

A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.

A stochastic, sequential algorithm.
At each round, it sees an observation in `𝓞`, then takes an action in `𝓐`, and finally receives
feedback in `𝓨`. The action is a random function of the past rounds and the current observation.

A kernel is a Markov kernel if every measure in its image is a probability measure.

A kernel from a measurable space `α` to another measurable space `β` is a measurable function
`κ : α → Measure β`. The measurable space structure on `MeasureTheory.Measure β` is given by
`MeasureTheory.Measure.instMeasurableSpace`. A map `κ : α → MeasureTheory.Measure β` is measurable
iff `∀ s : Set β, MeasurableSet s → Measurable (fun a ↦ κ a s)`.

An algorithm-environment sequence: a sequence of observations, actions and feedbacks generated
by an algorithm interacting with an environment.

A stationary environment without observations, in which the distribution of the next feedback
depends only on the last action.

The predicate `HasLaw X μ P` registers the fact that the random variable `X` has law `μ` under
the measure `P`, in other words that `P.map X = μ`. We also require `X` to be `AEMeasurable`,
to allow for nice interactions with operations on the codomain of `X`. See for instance
`HasLaw.comp`, `IndepFun.hasLaw_mul` and `IndepFun.hasLaw_add`.

Array of rewards by count, truncated at time `t`: the entry `(a, m)` is the reward received at
the `(m + 1)`-th pull of action `a` if that pull happened before time `t`, and the entry
`(m + 1, a)` of the auxiliary array `ω.2` otherwise.

This is an auxiliary definition used to prove results about the distribution of `rewardByCount`.

It is defined recursively: at time `t`, the
entry `(A t, pullCount A (A t) t)` is replaced by the reward `R' t`.
See `rewardByCountUntil_apply_of_lt_pullCount` and `rewardByCountUntil_apply_of_pullCount_le`.

The product measure of an arbitrary family of probability measures. It is defined as the unique
extension of the function which gives to cylinders the measure given by the associated product
measure.

It is defined via an `if ... then ... else` so that it can be manipulated without carrying
a proof that the measures are probability measures.

The binary product of measures. They are defined for arbitrary measures, but we basically
prove all properties under the assumption that at least one of them is s-finite.

Measure of an infinite stream of rewards from each action.