We consider special events of Borel sets with the aim to prove, that the set of the irrational numbers is an event of the Borel sets. The set of the natural numbers, the set of the integer numbers and the set of the rational numbers are countable, so we can use the literature [10] (pp. 78-81) as a basis for the similar construction of the proof. Next we prove, that different sets can construct the Borel sets [16] (pp. 9-10). Literature [16] (pp. 9-10) and [11] (pp. 11-12) gives an overview, that...
This article is about the Borel-Cantelli Lemma in probability theory. Necessary definitions and theorems are given in [10] and [7].
This article gives an elementary introduction to stochastic finance (in discrete time). A formalization of random variables is given and some elements of Borel sets are considered. Furthermore, special functions (for buying a present portfolio and the value of a portfolio in the future) and some statements about the relation between these functions are introduced. For details see: [8] (p. 185), [7] (pp. 12, 20), [6] (pp. 3-6).
We start with the definition of stopping time according to [4], p.283. We prove, that different definitions for stopping time can coincide. We give examples of stopping time using constant-functions or functions defined with the operator max or min (defined in [6], pp.37–38). Finally we give an example with some given filtration. Stopping time is very important for stochastic finance. A stopping time is the moment, where a certain event occurs ([7], p.372) and can be used together with stochastic...
First we give an implementation in Mizar [2] basic important definitions of stochastic finance, i.e. filtration ([9], pp. 183 and 185), adapted stochastic process ([9], p. 185) and predictable stochastic process ([6], p. 224). Second we give some concrete formalization and verification to real world examples. In article [8] we started to define random variables for a similar presentation to the book [6]. Here we continue this study. Next we define the stochastic process. For further definitions...
Download Results (CSV)