Hypothesis
A set is a collection of elements of some type α. In probability theory, a set is an event.
The universal set on a type α is the set containing all elements of α. It plays the role of state space or sample space in probability theory.
The Boolean values, true and false. Can also be used to represent “heads and tails” in probability theory.
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 β.
For example, Bool × Bool can be used to represent two successive tosses of a coin.
Icc a b is the left-closed right-closed interval \([a,b]\). For example, taking \(a=1\in \mathbb N\) and \(b=6\) we get the possible outcomes from tossing a die.
The type \(\mathbb R\) of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.
Attach \(\top \) to a type. For example \(\top \) could be \(+\infty \), a possible value of the measure of a set. WithTop is superficially the same as Option.
The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.
The complement of a set \(s\) is the set of elements not contained in \(s\).
Note that you should not use this definition directly, but instead write \(s^c\).
The intersection of two sets s and t is the set of elements contained in both s and t.
Note that you should not use this definition directly, but instead write s ∩ t.
The union of two sets s and t is the set of elements contained in either s or t.
Note that you should not use this definition directly, but instead write s ∪ t.
The singleton of an element \(a\) is the set with \(a\) as a single element.
Note that you should not use this definition directly, but instead write \(\{ a\} \).
In probability theory, \(a\) is an outcome and \(\{ a\} \) is an event.
𝒫 s is the set of all subsets of s.
In probability theory, this may be the family of all events; or some subsets may fail to be events.
Set.iUnion Indexed union of a family of sets.
A measurable space is a space equipped with a σ-algebra:
MeasurableSet (the sets in the \(\sigma \)-algebra \(\mathcal A\))
MeasurableSet.empty (\(\emptyset \in \mathcal A\) )
MeasurableSet.compl (\(\mathcal A\) is closed under complement)
MeasurableSet.iUnion (\(\mathcal A\) is closed under countable union, indexed by \(\mathbb N\))
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.
Probability measures are defined as the subtype of measures that have the property of being probability measures (i.e., their total mass is one).
The pushforward of a measure. It is defined to be 0 if f is not an almost everywhere measurable function.
For the pushforward of m along f, the outer measure on s is defined to be m (f ⁻¹’ s).
The pushforward of a probability measure.
It is suggested on page 4 of Jacod and Protter.
PMF.uniformOfFintype Uniform distribution, as in the Example on page 5 of Jacod and Protter.
0.1 Chapter 2
MeasurableSpace.generateFrom The \(\sigma \)-algebra generated by a family of sets.
MeasurableSpace.generateFrom The \(\sigma \)-algebra generated by a singleton. Not sure why it requires special mention.
The following results say that the trivial \(\sigma \)-algebra \(\bot \) can be generated in three ways: MeasurableSpace.generateFrom_empty, MeasurableSpace.generateFrom_singleton_empty, MeasurableSpace.generateFrom_singleton_univ.
The powerset as a \(\sigma \)-algebra is \(\top \), for example (\(\top \) : MeasurableSpace \(\mathbb R\)).
A topology on a given type.
Real.borel_eq_generateFrom_Iic_rat
Theorem 2.1 (page 8) in Jacod and Protter.
The fact that a measure is finitely additive is measure_union. The next property mentioned in JP is MeasureTheory.Measure.mono.
Theorem 2.3 is MeasureTheory.measure_biUnion_eq_iSup
Set indicator: Set.indicator