I have released version 1.9.0 of IsarMathLib. This is a quite large release with 10 new theory files and 155 new theorems, all contributed by Daniel de la Concepción Sáez. The first of the files contributed by Daniel (released in 1.8.0), Topology_ZF_4 about nets, filters and convergence in topological spaces is now presented on the isarmathlib.org site. The rest of Daniel’s contributions for now can be viewed in the proof document and the outline.
Here is a short description of what is in the new theories:
is a Markov chain on a state space 
. Distribution of the process 
and the numbers 
, 
, called transition probabilities. For simplicity let’s consider only time-homogeneous Markov chains where these numbers don’t depend on 
and let’s assume that the initial distribution is a point mass, i.e. 
for some 
. Then we can define a function 
, where for each 
the value 
is a distribution on 
. Here 
denotes the set of finitely supported nonnegative functions on 
. This is exactly the kind of distribution-valued function that is the right hand side operand of the 
operation from the
Formalized Mathematics 