Posts Tagged ‘mathematics’

IsarMathLib 1.9.0 released

July 26, 2013

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 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:



Markov chains

June 5, 2009

The approach taken in the Haskell’s probability library makes it especially convenient for modeling Markov chains.
Suppose  \{X_n\}_{n \in \mathbb{N}} is a Markov chain on a state space S. Distribution of the process \{X_n\}_{n \in \mathbb{N}} is determined by the distribution of X_0 and the numbers Pr(X_{n+1}=y | X_n = x), x,y \in S, n \in \mathbb{N}, called transition probabilities. For simplicity let’s consider only time-homogeneous Markov chains where these numbers don’t depend on n and let’s assume that the initial distribution is a point mass, i.e. X_0 = x_0 for some x_0\in S. Then we can define a function f: S \rightarrow Dist(S), where for each x \in S the value f(x) is a distribution on S defined by (f(x))(y) = Pr(X_{n+1}=y | X_n = x), x,y \in S, n \in \mathbb{N}. Here Dist(S) denotes the set of finitely supported nonnegative functions on S that sum up to 1. Conceptually, f(x) is the the distribution of the next value of the chain given the current value is x. This is exactly the kind of distribution-valued function that is the right hand side operand of the \leadsto operation from the previous post, which corresponds to the Haskell’s >>= operation in the probability monad. (more…)

Hello world!

September 22, 2007

This blog will be devoted to formalized mathematics.

Formalized mathematics is the craft of writing mathematical proofs in a formal proof language so that they can be verified by a machine.