Search Results

1 - 10 of 140 items :

Clear All
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.

Open access
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 xM 1 such that M 1(x) > N 1(x) and (∀yN 1)xy. It should be M 1(x) ⩾ N 1(x). Nevertheless we do not know whether xN 1 or not and cannot prove the contradiction. In the article we referred to [8], [9] and [10].

Open access
Basel Problem – Preliminaries

Summary

In the article we formalize in the Mizar system [4] preliminary facts needed to prove the Basel problem [7, 1]. Facts that are independent from the notion of structure are included here.

Open access
On Subnomials

Summary

While discussing the sum of consecutive powers as a result of division of two binomials W.W. Sawyer [12] observes

“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.”

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].
Open access
Basel Problem

Summary

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

n=11n2=π26
is formalized in the Mizar system [3]. This theorem is item #14 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.

Open access
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/.

Open access
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).

Open access
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].

Open access
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.

Open access
Chebyshev Distance

Summary

In [21], Marco Riccardi formalized that ℝN-basis n is a basis (in the algebraic sense defined in [26]) of Tn and in [20] he has formalized that Tn is second-countable, we build (in the topological sense defined in [23]) a denumerable base of Tn.

Then we introduce the n-dimensional intervals (interval in n-dimensional Euclidean space, pavé (borné) den [16], semi-intervalle (borné) den [22]).

We conclude with the definition of Chebyshev distance [11].

Open access