- Journal Details
- Format
- Journal
- eISSN
- 1898-9934
- ISSN
- 1426-2630
- First Published
- 09 Jun 2008
- Publication timeframe
- 4 times per year
- Languages
- English

#### Search

Open Access

#### Introduction to Stochastic Finance: Random Variables and Arbitrage Theory

Page range: 1 - 9

#### Abstract

Using the Mizar system [

In the third section, we introduce the definition of arbitrage opportunity, see (Def. 12). Next we show, that this definition can be characterized in a different way (Lemma 1.3. in [^{d}

We give an example in real world: Suppose you have some assets like bonds (riskless assets). Then we can fix our price for these bonds with _{fut}_{1} is a risk-neutral measure, see (21). This example shows the existence of some risk-neutral measure. If you find more than one of them, you can determine – with an additional conidition to the probability measures – whether a market model is arbitrage free or not (see Theorem 1.6. in [

A short graph for (21):

Suppose we have a portfolio with many (in this example infinitely many) assets. For asset

Let G be a sequence of random variables on Ω_{fut}_{1}, Borel sets. So you have many functions _{k}_{k}_{k}_{fut}_{1}, Borel sets. For every _{k}_{k}

Here, every probability measure of Ω_{fut}_{1} is a risk-neutral measure.

#### Keywords

- random variable
- arbitrage theory
- risk-neutral measure

#### MSC 2010

- 28A05
- 03B35

#### Abstract

We show that the set of all partial predicates over a set

The term “Kleene algebra” was introduced by A. Monteiro and D. Brignole in [

Algebras of partial predicates naturally arise in computability theory in the study on partial recursive predicates. They were studied in connection with non-classical logics [

Partial predicates over classes of mathematical models of data were used for formalizing semantics of computer programs in the composition-nominative approach to program formalization [

#### Keywords

- partial predicate
- Kleene algebra

#### MSC 2010

- 03B70
- 03G25
- 03B35

#### Abstract

Tim Makarios (with Isabelle/HOL^{1}) and John Harrison (with HOL-Light^{2}) shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [

With the Mizar system [

#### Keywords

- Tarski’s geometry axioms
- foundations of geometry
- Klein-Beltrami model

#### MSC 2010

- 51A05
- 51M10
- 03B35

#### Abstract

Tim Makarios (with Isabelle/HOL^{1}) and John Harrison (with HOL-Light^{2}) have shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [

With the Mizar system [

#### Keywords

- Tarski’s geometry axioms
- foundations of geometry
- Klein-Beltrami model

#### MSC 2010

- 51A05
- 51M10
- 03B35

Open Access

#### Fubini’s Theorem for Non-Negative or Non-Positive Functions

Page range: 49 - 67

#### Abstract

The goal of this article is to show Fubini’s theorem for non-negative or non-positive measurable functions [

On the other hand, the theorems obtained in this paper are more general and it can be easily extended to a general integrable function. Furthermore, it also can be easy to extend to functional space ^{p}

#### Keywords

- Fubini’ s theorem
- extended real-valued non-negative (or non-positive) measurable function

#### MSC 2010

- 28A35
- 03B35

Open Access

#### Sequences of Prime Reciprocals. Preliminaries

Page range: 69 - 79

#### Abstract

In the article we formalize some properties needed to prove that sequences of prime reciprocals are divergent. The aim is to show that the series exhibits log-log growth. We introduce some auxiliary notions as harmonic numbers, telescoping series, and prove some standard properties of logarithms and exponents absent in the Mizar Mathematical Library. At the end we proceed with square-free and square-containing parts of a natural number and reciprocals of corresponding products.

#### Keywords

- prime factorization
- sequence of prime reciprocals
- harmonic number

#### MSC 2010

- 11A51
- 03B35

#### Abstract

In this article, we define Diophantine sets using the Mizar formalism. We focus on selected properties of multivariate polynomials, i.e., functions of several variables to show finally that the class of Diophantine sets is closed with respect to the operations of union and intersection.

This article is the next in a series [

#### Keywords

- Hilbert’s 10th problem
- Pell’s equation
- multivariate polynomials

#### MSC 2010

- 11D45
- 03B35