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

A standard Borel space is a measurable space arising as the Borel sets of some Polish topology.
This is useful in situations where a space has no natural topology or
the natural topology in a space is non-Polish.

To endow a standard Borel space `α` with a compatible Polish topology, use
`letI := upgradeStandardBorel α`. One can then use `eq_borel_upgradeStandardBorel α` to
rewrite the `MeasurableSpace α` instance to `borel α t`, where `t` is the new topology.

`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.

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 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)`.

The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.

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.

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.

`IsBayesAlgEnvSeq Q κ alg E A Y P` states that there is a measure `P : Measure Ω` such
that the parameter `E : Ω → 𝓔` has law `Q` and that the sequences of actions `A : ℕ → Ω → 𝓐`
and feedbacks `Y : ℕ → Ω → 𝓨` are generated by the algorithm `alg : Algorithm Unit 𝓐 𝓨`
interacting with an underlying environment that depends on `E` and `κ`
(`stationaryEnv (κ.sectR (E ω))`).

This is `IsAlgEnvSeq` for the announcing environment `bayesStationaryEnv Q κ` and the algorithm
`alg.comapObs (fun _ ↦ ())` that ignores the announced parameter: the observation at every round
is `E ω`.

`f.Eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in atTop, p x`
means that `p` holds true for sufficiently large `x`.

Predicate stating that the conditional distribution of `Y` given `X` under the measure `P`
is equal to the kernel `κ`.

`obs n` is the observation at time `n`. This is a random variable on the measurable space
`ℕ → Round 𝓞 𝓐 𝓨`.

`hist n` is the history before time `n`: the rounds at times `0, ..., n - 1`.
This is a random variable on the measurable space `ℕ → Round 𝓞 𝓐 𝓨`.

Constant kernel, which always returns the same measure.

History of `n` complete rounds; `n = 0` is the empty history.

The dirac measure.

The only element of the unit type.

It can be written as an empty tuple: `()`.

**Regular conditional probability distribution**: kernel associated with the conditional
expectation of `Y` given `X`.
For almost all `a`, `condDistrib Y X μ` evaluated at `X a` and a measurable set `s` is equal to
the conditional expectation `μ⟦Y ⁻¹' s | mβ.comap X⟧ a`. It also satisfies the equality
`μ[(fun a => f (X a, Y a)) | mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂(condDistrib Y X μ (X a))`
for all integrable functions `f`.

A random variable that gives the sequence of rounds.

The observation process of an algorithm-environment sequence without observations.