###### Binary Representation of Natural Numbers

## Summary

Binary representation of integers [5], [3] and arithmetic operations on them have already been introduced in Mizar Mathematical Library [8, 7, 6, 4]. However, these articles formalize the notion of integers as mapped into a certain length tuple of boolean values.

In this article we formalize, by means of Mizar system [2], [1], the binary representation of natural numbers which maps ℕ into bitstreams.

###### On Multiset Ordering

## Summary

Formalization of a part of [11]. Unfortunately, not all is possible to be formalized. Namely, in the paper there is a mistake in the proof of Lemma 3. It states that there exists *x* ∈ *M*
_{1} such that *M*
_{1}(*x*) > *N*
_{1}(*x*) and (∀*y* ∈ *N*
_{1})*x* ⊀ *y*. It should be *M*
_{1}(*x*) ⩾ *N*
_{1}(*x*). Nevertheless we do not know whether *x* ∈ *N*
_{1} or not and cannot prove the contradiction. In the article we referred to [8], [9] and [10].

###### On Subnomials

## Summary

It’s worth noticing that the first issue involves a simple arithmetical division of 99...9 by 9. While the above notion seems not have changed over the last 50 years, it reflects only a special case of a broader class of problems involving two variables. It seems strange, that while binomial formula is discussed and studied widely [7], [8], little research is done on its counterpart with all coefficients equal to one, which we will call here the subnomial. The study focuses on its basic properties and applies it to some simple problems usually proven by induction [6].“It is a curious fact that most algebra textbooks give our ast result twice. It appears in two different chapters and usually there is no mention in either of these that it also occurs in the other. The first chapter, of course, is that on factors. The second is that on geometrical progressions. Geometrical progressions are involved in nearly all financial questions involving compound interest – mortgages, annuities, etc.”

###### Basel Problem

## Summary

A rigorous elementary proof of the Basel problem [6, 1]

###### Bertrand’s Ballot Theorem

## Summary

In this article we formalize the Bertrand’s Ballot Theorem based on [17]. Suppose that in an election we have two candidates: *A* that receives *n* votes and *B* that receives *k* votes, and additionally *n ≥ k*. Then this theorem states that the probability of the situation where *A* maintains more votes than *B* throughout the counting of the ballots is equal to (*n − k*)/(*n* + *k*).

This theorem is item #30 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.

###### Introduction to Stopping Time in Stochastic Finance Theory

## Summary

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 processes ([4], p.283). Look at the following example: we install a function ST: {1,2,3,4} → {0, 1, 2} ∪ {+∞}, we define:

a. ST(1)=1, ST(2)=1, ST(3)=2, ST(4)=2.

b. The set {0,1,2} consists of time points: 0=now,1=tomorrow,2=the day after tomorrow.

We can prove:

c. {w, where w is Element of Ω: ST.w=0}=∅ & {w, where w is Element of Ω: ST.w=1}={1,2} & {w, where w is Element of Ω: ST.w=2}={3,4} and

ST is a stopping time.

We use a function Filt as Filtration of {0,1,2}, Σ where Filt(0)=Ω* _{now}*, Filt(1)=Ω

_{fut}_{1}and Filt(2)=Ω

_{fut}_{2}. From a., b. and c. we know that:

d. {w, where w is Element of Ω: ST.w=0} in Ω* _{now}* and

{w, where w is Element of Ω: ST.w=1} in Ω_{fut}_{1} and

{w, where w is Element of Ω: ST.w=2} in Ω_{fut}_{2}.

The sets in d. are events, which occur at the time points 0(=now), 1(=tomorrow) or 2(=the day after tomorrow), see also [7], p.371. Suppose we have ST(1)=+∞, then this means that for 1 the corresponding event never occurs.

As an interpretation for our installed functions consider the given adapted stochastic process in the article [5].

ST(1)=1 means, that the given element 1 in {1,2,3,4} is stopped in 1 (=tomorrow). That tells us, that we have to look at the value *f*
_{2}(1) which is equal to 80. The same argumentation can be applied for the element 2 in {1,2,3,4}.

ST(3)=2 means, that the given element 3 in {1,2,3,4} is stopped in 2 (=the day after tomorrow). That tells us, that we have to look at the value *f*
_{3}(3) which is equal to 100.

ST(4)=2 means, that the given element 4 in {1,2,3,4} is stopped in 2 (=the day after tomorrow). That tells us, that we have to look at the value *f*
_{3}(4) which is equal to 120.

In the real world, these functions can be used for questions like: when does the share price exceed a certain limit? (see [7], p.372).

###### On Roots of Polynomials and Algebraically Closed Fields

## Summary

In this article we further extend the algebraic theory of polynomial rings in Mizar [1, 2, 3]. We deal with roots and multiple roots of polynomials and show that both the real numbers and finite domains are not algebraically closed [5, 7]. We also prove the identity theorem for polynomials and that the number of multiple roots is bounded by the polynomial’s degree [4, 6].

###### Algebraic Numbers

## Summary

This article provides definitions and examples upon an integral element of unital commutative rings. An algebraic number is also treated as consequence of a concept of “integral”. Definitions for an integral closure, an algebraic integer and a transcendental numbers [14], [1], [10] and [7] are included as well. As an application of an algebraic number, this article includes a formal proof of a ring extension of rational number field ℚ induced by substitution of an algebraic number to the polynomial ring of ℚ[*x*] turns to be a field.

###### Chebyshev Distance

## Summary

In [21], Marco Riccardi formalized that ℝN-basis *n* is a basis (in the algebraic sense defined in [26]) of

Then we introduce the *n*-dimensional intervals (interval in *n*-dimensional Euclidean space, *pavé (borné) de* ℝ* ^{n}*
[16],

*semi-intervalle (borné) de*ℝ

*[22]).*

^{n}We conclude with the definition of Chebyshev distance [11].